1.1 --- a/src/Provers/clasimp.ML	Wed Sep 01 21:22:38 1999 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Wed Sep 01 21:22:56 1999 +0200
     1.3 @@ -156,10 +156,10 @@
     1.4  val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
     1.5  
     1.6  fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
     1.7 -  ALLGOALS (Method.same_tac facts) THEN tac (get_local_clasimpset ctxt));
     1.8 +  ALLGOALS (Method.insert_tac facts) THEN tac (get_local_clasimpset ctxt));
     1.9  
    1.10  fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
    1.11 -  FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_clasimpset ctxt)));
    1.12 +  FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_clasimpset ctxt)));
    1.13  
    1.14  val clasimp_method = clasimp_args o clasimp_meth;
    1.15  val clasimp_method' = clasimp_args o clasimp_meth';