src/CCL/typecheck.ML
changeset 642 0db578095e6a
parent 289 78541329ff35
child 757 2ca12511676d
     1.1 --- a/src/CCL/typecheck.ML	Wed Oct 12 16:38:58 1994 +0100
     1.2 +++ b/src/CCL/typecheck.ML	Wed Oct 19 09:23:56 1994 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  val Subtype_canTs = 
     1.5         let fun tac prems = cut_facts_tac prems 1 THEN
     1.6                  REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
     1.7 -                        eresolve_tac [SubtypeE] 1)
     1.8 +                        etac SubtypeE 1)
     1.9             fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
    1.10         in map solve
    1.11             ["P(one) ==> one : {x:Unit.P(x)}",
    1.12 @@ -31,7 +31,7 @@
    1.13  val Subtype_canTs = 
    1.14         let fun tac prems = cut_facts_tac prems 1 THEN
    1.15                  REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
    1.16 -                        eresolve_tac [SubtypeE] 1)
    1.17 +                        etac SubtypeE 1)
    1.18             fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
    1.19         in map solve
    1.20             ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
    1.21 @@ -44,8 +44,8 @@
    1.22  val prems = goal Type.thy
    1.23       "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B";
    1.24  by (cut_facts_tac prems 1);
    1.25 -be (letB RS ssubst) 1;
    1.26 -ba 1;
    1.27 +by (etac (letB RS ssubst) 1);
    1.28 +by (assume_tac 1);
    1.29  val letT = result();
    1.30  
    1.31  val prems = goal Type.thy