# HG changeset patch
# User clasohm
# Date 764336576 -3600
# Node ID 78541329ff35a03f20ac3588bdb1fa2a0ac119c9
# Parent  b00ce6a1fe27eb9a4d46200696ec9dfa2bb36ccf
changed "." to "$" to eliminate ambiguity

diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/Hered.ML
--- a/src/CCL/Hered.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Hered.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -70,7 +70,7 @@
                            "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]);
@@ -108,7 +108,7 @@
 \                         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 ***)
 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/Term.ML
--- a/src/CCL/Term.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Term.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -90,10 +90,10 @@
 val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
 
 val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
-val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
+val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
 val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
 val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
-val lrecBcons  = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
+val lrecBcons  = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
 val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
 
 val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
@@ -120,12 +120,12 @@
                ["(inl(a) = inl(a')) <-> (a=a')",
                 "(inr(a) = inr(a')) <-> (a=a')",
                 "(succ(a) = succ(a')) <-> (a=a')",
-                "(a.b = a'.b') <-> (a=a' & b=b')"];
+                "(a$b = a'$b') <-> (a=a' & b=b')"];
 
 (*** Constructors are distinct ***)
 
 val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
-                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
+                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
 
 (*** Rules for pre-order [= ***)
 
@@ -136,7 +136,7 @@
   val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
                                 "inr(b) [= inr(b') <-> b [= b'",
                                 "succ(n) [= succ(n') <-> n [= n'",
-                                "x.xs [= x'.xs' <-> x [= x'  & xs [= xs'"];
+                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"];
 end;
 
 (*** Rewriting and Proving ***)
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Term.thy	Tue Mar 22 12:42:56 1994 +0100
@@ -28,7 +28,7 @@
   nrec       ::	      "[i,i,[i,i]=>i]=>i"
 
   nil        ::       "i"                    ("([])")
-  "."        ::       "[i,i]=>i"             (infixr 80)
+  "$"        ::       "[i,i]=>i"             (infixr 80)
   lcase      ::	      "[i,i,[i,i]=>i]=>i"
   lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
 
@@ -60,7 +60,7 @@
   ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
   nil_def	              "[] == inl(one)"
-  cons_def                   "h.t == inr(<h,t>)"
+  cons_def                   "h$t == inr(<h,t>)"
   lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
 
diff -r b00ce6a1fe27 -r 78541329ff35 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;
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/Wfd.ML
--- a/src/CCL/Wfd.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Wfd.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -179,7 +179,7 @@
 by (fast_tac set_cs 1);
 val NatPRXH = result();
 
-goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
+goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
 val ListPRXH = result();
 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Wfd.thy	Tue Mar 22 12:42:56 1994 +0100
@@ -30,5 +30,5 @@
   "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
 
   NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
-  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
+  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
 end
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/coinduction.ML
--- a/src/CCL/coinduction.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/coinduction.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -60,7 +60,7 @@
        "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
        "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); \
 \          <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> \
-\       <h.t,h'.t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
+\       <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
 
 fun POgen_tac (rla,rlb) i =
        SELECT_GOAL (safe_tac ccl_cs) i THEN
@@ -90,7 +90,7 @@
  "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
 \          <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \
-\       <h.t,h'.t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
+\       <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
 
 fun EQgen_raw_tac i =
        (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/eval.ML
--- a/src/CCL/eval.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/eval.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -58,11 +58,11 @@
               "[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c",
               "[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c",
               "[] ---> []",
-              "h.t ---> h.t",
+              "h$t ---> h$t",
               "[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c",
-              "[| l ---> x.xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
+              "[| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
               "[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c",
-              "[| l--->x.xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
+              "[| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
 
 EVal_rls := !EVal_rls @ V_rls;
 
@@ -93,12 +93,12 @@
 (* Reverse *)
 
 val prems = goal thy
-    "letrec id l be lcase(l,[],%x xs.x.id(xs)) \
-\              in id(zero.succ(zero).[]) ---> ?a";
+    "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
+\              in id(zero$succ(zero)$[]) ---> ?a";
 by (ceval_tac []);
 
 val prems = goal thy
-    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x.[],%y ys g.y.g)) \
-\              in rev(zero.succ(zero).(succ((lam x.x)`succ(zero))).([])) ---> ?a";
+    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
+\              in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
 by (ceval_tac []);
 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/hered.ML
--- a/src/CCL/hered.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/hered.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -70,7 +70,7 @@
                            "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]);
@@ -108,7 +108,7 @@
 \                         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 ***)
 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/term.ML
--- a/src/CCL/term.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/term.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -90,10 +90,10 @@
 val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
 
 val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
-val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
+val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
 val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
 val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
-val lrecBcons  = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
+val lrecBcons  = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
 val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
 
 val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
@@ -120,12 +120,12 @@
                ["(inl(a) = inl(a')) <-> (a=a')",
                 "(inr(a) = inr(a')) <-> (a=a')",
                 "(succ(a) = succ(a')) <-> (a=a')",
-                "(a.b = a'.b') <-> (a=a' & b=b')"];
+                "(a$b = a'$b') <-> (a=a' & b=b')"];
 
 (*** Constructors are distinct ***)
 
 val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
-                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
+                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
 
 (*** Rules for pre-order [= ***)
 
@@ -136,7 +136,7 @@
   val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
                                 "inr(b) [= inr(b') <-> b [= b'",
                                 "succ(n) [= succ(n') <-> n [= n'",
-                                "x.xs [= x'.xs' <-> x [= x'  & xs [= xs'"];
+                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"];
 end;
 
 (*** Rewriting and Proving ***)
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/term.thy
--- a/src/CCL/term.thy	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/term.thy	Tue Mar 22 12:42:56 1994 +0100
@@ -28,7 +28,7 @@
   nrec       ::	      "[i,i,[i,i]=>i]=>i"
 
   nil        ::       "i"                    ("([])")
-  "."        ::       "[i,i]=>i"             (infixr 80)
+  "$"        ::       "[i,i]=>i"             (infixr 80)
   lcase      ::	      "[i,i,[i,i]=>i]=>i"
   lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
 
@@ -60,7 +60,7 @@
   ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
   nil_def	              "[] == inl(one)"
-  cons_def                   "h.t == inr(<h,t>)"
+  cons_def                   "h$t == inr(<h,t>)"
   lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
 
diff -r b00ce6a1fe27 -r 78541329ff35 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;
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/typecheck.ML
--- a/src/CCL/typecheck.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/typecheck.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -25,7 +25,7 @@
             "P(zero) ==> zero : {x:Nat.P(x)}",
             "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
             "P([]) ==> [] : {x:List(A).P(x)}",
-            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
+            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
         ] end;
 *)
 val Subtype_canTs = 
@@ -38,7 +38,7 @@
             "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
             "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
             "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
-            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
+            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
         ] end;
 
 val prems = goal Type.thy
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/wfd.ML
--- a/src/CCL/wfd.ML	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/wfd.ML	Tue Mar 22 12:42:56 1994 +0100
@@ -179,7 +179,7 @@
 by (fast_tac set_cs 1);
 val NatPRXH = result();
 
-goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
+goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
 val ListPRXH = result();
 
diff -r b00ce6a1fe27 -r 78541329ff35 src/CCL/wfd.thy
--- a/src/CCL/wfd.thy	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/wfd.thy	Tue Mar 22 12:42:56 1994 +0100
@@ -30,5 +30,5 @@
   "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
 
   NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
-  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
+  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
 end