# HG changeset patch
# User wenzelm
# Date 1154000587 -7200
# Node ID da4ec4b48be1c4f946baaab8fb942f608f1957b8
# Parent  e0f9e8a6556b0e71cad004c7d56598db529887b7
Assumption.assume;

diff -r e0f9e8a6556b -r da4ec4b48be1 src/Pure/old_goals.ML
--- 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