# HG changeset patch
# User paulson
# Date 1107355384 -3600
# Node ID 06a32fe35ec34af77de422626146fd87402d8d46
# Parent  e93a3badc2bc49b96d1defc9c5677455f94321b1
improved handling of chained facts

diff -r e93a3badc2bc -r 06a32fe35ec3 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Wed Feb 02 10:16:33 2005 +0100
+++ b/src/Provers/eqsubst.ML	Wed Feb 02 15:43:04 2005 +0100
@@ -117,8 +117,8 @@
    the first one, then the second etc *)
 fun eqsubst_meth inthms =
     Method.METHOD 
-      (fn facts =>
-          HEADGOAL (eqsubst_tac inthms THEN' Method.insert_tac facts));
+      (fn facts =>  (*first, insert chained facts*)
+          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac inthms));
 
 
 fun apply_subst_in_asm rule cfvs i th matchseq = 
@@ -184,8 +184,9 @@
    the first one, then the second etc *)
 fun eqsubst_asm_meth inthms =
     Method.METHOD 
-      (fn facts =>
-          HEADGOAL (eqsubst_asm_tac inthms THEN' Method.insert_tac facts));
+      (fn facts =>  (*first, insert chained facts*)
+          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms));
+
 
 (* combination method that takes a flag (true indicates that subst
 should be done to an assumption, false = apply to the conclusion of