diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 729a8fb431..915a6fa1f2 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -151,13 +151,16 @@ let undefined = "undefined";
 let is_undefined = match(regexp("^" ++ undefined ++ "$"));
 
 let is_livelit = str => {
-  let re = regexp("^(ll)([a-z][A-Za-z0-9_]*)$");
-  // print_endline("is_livelit");
-  // print_endline(str);
+  let re = regexp("^(\\^)([A-Za-z0-9_]*)$");
   let result = match(re, str);
-  // print_endline(string_of_bool(result));
   result;
 };
+let parse_livelit = str =>
+  if (String.length(str) > 1 && String.sub(str, 0, 1) == "^") {
+    String.sub(str, 1, String.length(str) - 1);
+  } else {
+    "invalid form";
+  };
 
 let var_regexp =
   regexp(
@@ -354,20 +357,34 @@ let delims: list(Token.t) =
   |> List.sort_uniq(compare);
 
 let atomic_molds: Token.t => list(Mold.t) =
-  s =>
+  s => {
+    print_endline("atomic_molds");
+    print_endline(s);
     List.fold_left(
       (acc, (_, (test, molds))) => test(s) ? molds @ acc : acc,
       [],
       atomic_forms,
     );
+  };
 
-let is_atomic = t => atomic_molds(t) != [];
+let is_atomic = t => {
+  print_endline("is_atomic");
+  print_endline(t);
+  atomic_molds(t) != [];
+};
 
 let is_delim = t => List.mem(t, delims);
 
-let is_valid_token = t => is_atomic(t) || is_secondary(t) || is_delim(t);
+let is_valid_token = t => {
+  print_endline("is_valid_token");
+  print_endline(t);
+  is_atomic(t) || is_secondary(t) || is_delim(t);
+};
 
 let mk_atomic = (sort: Sort.t, t: Token.t) => {
+  print_endline("mk_atomic");
+  print_endline(t);
+
   assert(is_atomic(t));
   mk(ss, [t], Mold.(mk_op(sort, [])));
 };
diff --git a/src/haz3lcore/lang/Molds.re b/src/haz3lcore/lang/Molds.re
index c754dac288..3a44d5259c 100644
--- a/src/haz3lcore/lang/Molds.re
+++ b/src/haz3lcore/lang/Molds.re
@@ -17,7 +17,10 @@ let forms_assoc: list((Label.t, list(Mold.t))) =
     Form.forms,
   );
 
-let get = (label: Label.t): list(Mold.t) =>
+let get = (label: Label.t): list(Mold.t) => {
+  print_endline("Molds.get");
+  print_endline(String.concat(" ", label));
+
   switch (label, List.assoc_opt(label, forms_assoc)) {
   | ([t], Some(molds)) when Form.atomic_molds(t) != [] =>
     Form.atomic_molds(t) @ molds
@@ -54,6 +57,7 @@ let get = (label: Label.t): list(Mold.t) =>
     );
     [Mold.mk_op(Any, [])];
   };
+};
 
 let delayed_expansions: expansions =
   List.filter_map(
diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re
index 3812b0e83f..dc73a1a363 100644
--- a/src/haz3lcore/lang/term/IdTagged.re
+++ b/src/haz3lcore/lang/term/IdTagged.re
@@ -15,10 +15,10 @@ type t('a) = {
 };
 
 // To be used if you want to remove the id from the debug output
-// let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit =
-//   (fmt_a, formatter, ta) => {
-//     fmt_a(formatter, ta.term);
-//   };
+let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit =
+  (fmt_a, formatter, ta) => {
+    fmt_a(formatter, ta.term);
+  };
 let fresh = term => {
   {ids: [Id.mk()], copied: false, term};
 };
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index f95577d092..b003b7566f 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -189,7 +189,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         ret(String(Form.strip_quotes(t)))
       | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t)))
       | ([t], []) when Form.is_livelit(t) =>
-        ret(LivelitInvocation("livelit name"))
+        ret(LivelitInvocation(Form.parse_livelit(t)))
       | ([t], []) when Form.is_var(t) => ret(Var(t))
       | ([t], []) when Form.is_ctr(t) =>
         ret(Constructor(t, Unknown(Internal) |> Typ.temp))
@@ -258,6 +258,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           term: Deferral(InAp),
         };
         switch (arg.term) {
+        | Var(l) when Form.is_livelit(l) =>
+          ret(LivelitInvocation(Form.parse_livelit(l)))
         | _ when UExp.is_deferral(arg) =>
           ret(DeferredAp(l, [use_deferral(arg)]))
         | Tuple(es) when List.exists(UExp.is_deferral, es) => (
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 281ce71fd3..ee3eeca052 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -396,6 +396,7 @@ and Exp: {
       ClosureEnvironment.id_equal(c1, c2) && fast_equal(e1, e2)
     | (Cons(e1, e2), Cons(e3, e4)) =>
       fast_equal(e1, e3) && fast_equal(e2, e4)
+    | (LivelitInvocation(s1), LivelitInvocation(s2)) => s1 == s2
     | (ListConcat(e1, e2), ListConcat(e3, e4)) =>
       fast_equal(e1, e3) && fast_equal(e2, e4)
     | (UnOp(o1, e1), UnOp(o2, e2)) => o1 == o2 && fast_equal(e1, e2)
diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re
index 82eee683b6..dff49df747 100644
--- a/test/Test_MakeTerm.re
+++ b/test/Test_MakeTerm.re
@@ -67,4 +67,7 @@ let tests = [
       "let    = fun x ->   in  ",
     )
   }),
+  test_case("Livelit Invocation", `Quick, () => {
+    exp_check(LivelitInvocation("slider") |> Exp.fresh, "^slider")
+  }),
 ];