# HG changeset patch
# User wenzelm
# Date 1004134199 -7200
# Node ID a6608d44a46b69e717c6f7e9026a0fd5eab4d09d
# Parent  4c6585866fb213659f3e3f42b5b1cd54e9246bf5
impose hyps on initial goal configuration (prevents res_inst_tac problems);

diff -r 4c6585866fb2 -r a6608d44a46b 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. *)