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