src/CCL/Type.ML

--- a/src/CCL/Type.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Type.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -183,9 +183,9 @@
 val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
 
 val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
-val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
-val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
-val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
+val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
+val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
+val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
 
 val iXHs = [NatXH,ListXH];
 val icase_rls = XH_to_Es iXHs;
@@ -198,7 +198,7 @@
 val zeroT = icanT_tac "zero : Nat";
 val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
 val nilT  = icanT_tac "[] : List(A)";
-val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
+val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h$t : List(A)";
 
 val icanTs = [zeroT,succT,nilT,consT];
 
@@ -209,7 +209,7 @@
 
 val lcaseT = incanT_tac
      "[| l:List(A); l=[] ==> b:C([]); \
-\        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
+\        !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
 \     lcase(l,b,c) : C(l)";
 
 val incanTs = [ncaseT,lcaseT];
@@ -230,7 +230,7 @@
 
 val List_ind = ind_tac
      "[| l:List(A); P([]); \
-\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
+\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
 \     P(l)";
 
 val inds = [Nat_ind,List_ind];
@@ -250,7 +250,7 @@
 
 val lrecT = prec_tac
      "[| l:List(A); b:C([]); \
-\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
+\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>  \
 \     lrec(l,b,c) : C(l)";
 
 val precTs = [nrecT,lrecT];
@@ -300,7 +300,7 @@
 (* EG *)
 
 val prems = goal Type.thy 
-    "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
+    "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
 by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
 br (letrecB RS ssubst) 1;
 bw cons_def;