Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
impose hyps on initial goal configuration (prevents res_inst_tac problems);
authorwenzelm
Sat, 27 Oct 2001 00:09:59 +0200
changeset 11963 a6608d44a46b
parent 11962 4c6585866fb2
child 11964 828ea309dc21
impose hyps on initial goal configuration (prevents res_inst_tac problems);
src/Pure/goals.ML file | annotate | diff | comparison | revisions 
--- 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. *)
isabelle