src/CCL/typecheck.ML

             "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)}",
             "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 = 
        let fun tac prems = cut_facts_tac prems 1 THEN
                 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE

        in map solve
            ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
             "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
      "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B";
 by (cut_facts_tac prems 1);