src/Pure/old_goals.ML
changeset 20229 da4ec4b48be1
parent 19053 358c0eb6d785
child 20322 c80539928948
     1.1 --- a/src/Pure/old_goals.ML	Thu Jul 27 13:43:06 2006 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Thu Jul 27 13:43:07 2006 +0200
     1.3 @@ -380,7 +380,7 @@
     1.4      val _ = warn_obsolete ();
     1.5      val As = Drule.strip_imp_prems G;
     1.6      val B = Drule.strip_imp_concl G;
     1.7 -    val asms = map (Goal.norm_hhf o Thm.assume) As;
     1.8 +    val asms = map Assumption.assume As;
     1.9      fun check NONE = error "prove_goal: tactic failed"
    1.10        | check (SOME (thm, _)) = (case nprems_of thm of
    1.11              0 => thm