src/HOL/ex/MT.ML
changeset 4353 d565d2197a5f
parent 4153 e534c4c32d54
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/ex/MT.ML	Wed Dec 03 10:52:17 1997 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Dec 03 11:00:24 1997 +0100
     1.3 @@ -418,7 +418,7 @@
     1.4  fun elab_e_elim_tac p = 
     1.5    ( (rtac elab_elim 1) THEN 
     1.6      (resolve_tac p 1) THEN 
     1.7 -    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
     1.8 +    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
     1.9    );
    1.10  
    1.11  val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";