src/HOL/Hoare/hoare_tac.ML
changeset 42793 88bee9f6eec7
parent 41449 7339f0e7c513
child 44241 7943b69f0188
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4      val MsetT = fastype_of big_Collect;
     1.5      fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
     1.6      val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
     1.7 -    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
     1.8 +    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
     1.9   in (vars, th) end;
    1.10  
    1.11  end;