src/CCL/Hered.ML

                            "inl(a) : HTT <-> a : HTT",
                            "inr(b) : HTT <-> b : HTT",
                            "zero : HTT",
                            "succ(n) : HTT <-> n : HTT",
                            "[] : HTT",
-                           "x.xs : HTT <-> x : HTT & xs : HTT"];
+                           "x$xs : HTT <-> x : HTT & xs : HTT"];
 end;
 
 val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
 
 (*** Coinduction for HTT ***)

         "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
         "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
 \                         succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
         "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
         "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
-\                         h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
+\                         h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
 
 (*** Formation Rules for Types ***)
 
 goal Hered.thy "Unit <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);