1.1 --- a/src/Provers/eqsubst.ML	Wed Feb 02 10:16:33 2005 +0100
     1.2 +++ b/src/Provers/eqsubst.ML	Wed Feb 02 15:43:04 2005 +0100
     1.3 @@ -117,8 +117,8 @@
     1.4     the first one, then the second etc *)
     1.5  fun eqsubst_meth inthms =
     1.6      Method.METHOD 
     1.7 -      (fn facts =>
     1.8 -          HEADGOAL (eqsubst_tac inthms THEN' Method.insert_tac facts));
     1.9 +      (fn facts =>  (*first, insert chained facts*)
    1.10 +          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac inthms));
    1.11  
    1.12  
    1.13  fun apply_subst_in_asm rule cfvs i th matchseq = 
    1.14 @@ -184,8 +184,9 @@
    1.15     the first one, then the second etc *)
    1.16  fun eqsubst_asm_meth inthms =
    1.17      Method.METHOD 
    1.18 -      (fn facts =>
    1.19 -          HEADGOAL (eqsubst_asm_tac inthms THEN' Method.insert_tac facts));
    1.20 +      (fn facts =>  (*first, insert chained facts*)
    1.21 +          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms));
    1.22 +
    1.23  
    1.24  (* combination method that takes a flag (true indicates that subst
    1.25  should be done to an assumption, false = apply to the conclusion of