Assumption.assume;

--- a/src/Pure/old_goals.ML	Thu Jul 27 13:43:06 2006 +0200
+++ b/src/Pure/old_goals.ML	Thu Jul 27 13:43:07 2006 +0200
@@ -380,7 +380,7 @@
     val _ = warn_obsolete ();
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
-    val asms = map (Goal.norm_hhf o Thm.assume) As;
+    val asms = map Assumption.assume As;
     fun check NONE = error "prove_goal: tactic failed"
       | check (SOME (thm, _)) = (case nprems_of thm of
             0 => thm