--- a/src/Pure/goals.ML	Fri Oct 28 22:27:55 2005 +0200
+++ b/src/Pure/goals.ML	Fri Oct 28 22:27:56 2005 +0200
@@ -381,7 +381,7 @@
     val _ = warn_obsolete ();
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
-    val asms = map (Goal.norm_hhf_rule o assume) As;
+    val asms = map (Goal.norm_hhf o Thm.assume) As;
     fun check NONE = error "prove_goal: tactic failed"
       | check (SOME (thm, _)) = (case nprems_of thm of
             0 => thm