src/Pure/goals.ML

--- a/src/Pure/goals.ML	Sat Oct 27 00:07:48 2001 +0200
+++ b/src/Pure/goals.ML	Sat Oct 27 00:09:59 2001 +0200
@@ -212,9 +212,9 @@
             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);
       val cAs = map (cterm_of sign) As;
-      val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs;
+      val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
       val cB = cterm_of sign B;
-      val st0 = let val st = Drule.mk_triv_goal cB
+      val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
                 in  rewrite_goals_rule rths st end
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)