src/CCL/typecheck.ML
changeset 289 78541329ff35
parent 0 a5a9c433f639
child 642 0db578095e6a
     1.1 --- a/src/CCL/typecheck.ML	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/typecheck.ML	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4              "P(zero) ==> zero : {x:Nat.P(x)}",
     1.5              "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
     1.6              "P([]) ==> [] : {x:List(A).P(x)}",
     1.7 -            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
     1.8 +            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
     1.9          ] end;
    1.10  *)
    1.11  val Subtype_canTs = 
    1.12 @@ -38,7 +38,7 @@
    1.13              "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
    1.14              "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
    1.15              "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
    1.16 -            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
    1.17 +            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
    1.18          ] end;
    1.19  
    1.20  val prems = goal Type.thy