1.1 --- a/src/Provers/clasimp.ML	Thu Sep 24 17:17:14 1998 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Thu Sep 24 17:17:56 1998 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  simplifier.ML, classical.ML, blast.ML).
     1.5  *)
     1.6  
     1.7 -infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
     1.8 -	addsimps2 delsimps2 addcongs2 delcongs2;
     1.9 +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2;
    1.10  infix 4 addSss addss;
    1.11  
    1.12  signature CLASIMP_DATA =
    1.13 @@ -16,10 +15,6 @@
    1.14    structure Classical: CLASSICAL
    1.15    structure Blast: BLAST
    1.16    sharing type Classical.claset = Blast.claset
    1.17 -  val addcongs: Simplifier.simpset * thm list -> Simplifier.simpset
    1.18 -  val delcongs: Simplifier.simpset * thm list -> Simplifier.simpset
    1.19 -  val addSaltern: Classical.claset * (string * (int -> tactic)) -> Classical.claset
    1.20 -  val addbefore: Classical.claset * (string * (int -> tactic)) -> Classical.claset
    1.21  end
    1.22  
    1.23  signature CLASIMP =
    1.24 @@ -77,15 +72,13 @@
    1.25  fun op addDs2    arg = pair_upd1 Classical.addDs arg;
    1.26  fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg;
    1.27  fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg;
    1.28 -fun op addcongs2 arg = pair_upd2 Data.addcongs arg;
    1.29 -fun op delcongs2 arg = pair_upd2 Data.delcongs arg;
    1.30  
    1.31  (*Add a simpset to a classical set!*)
    1.32  (*Caution: only one simpset added can be added by each of addSss and addss*)
    1.33 -fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
    1.34 -			CHANGED o Simplifier.safe_asm_full_simp_tac ss);
    1.35 -fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", 
    1.36 -			CHANGED o Simplifier.asm_full_simp_tac ss);
    1.37 +fun cs addSss ss = op Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
    1.38 +			    CHANGED o Simplifier.safe_asm_full_simp_tac ss));
    1.39 +fun cs addss  ss = op Classical.addbefore  (cs, ("asm_full_simp_tac", 
    1.40 +			    CHANGED o Simplifier.asm_full_simp_tac ss));
    1.41  
    1.42  (* tacticals *)
    1.43  
    1.44 @@ -104,7 +97,8 @@
    1.45  (* auto_tac *)
    1.46  
    1.47  fun blast_depth_tac cs m i thm =
    1.48 -  Blast.depth_tac cs m i thm handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    1.49 +    Blast.depth_tac cs m i thm 
    1.50 +      handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    1.51  
    1.52  (* a variant of depth_tac that avoids interference of the simplifier 
    1.53     with dup_step_tac when they are combined by auto_tac *)
    1.54 @@ -123,9 +117,9 @@
    1.55  fun mk_auto_tac (cs, ss) m n =
    1.56      let val cs' = cs addss ss
    1.57          val maintac = 
    1.58 -          blast_depth_tac cs m		(*fast but can't use addss*)
    1.59 +          blast_depth_tac cs m		(* fast but can't use addss *)
    1.60            ORELSE'
    1.61 -          nodup_depth_tac cs' n;	(*slower but more general*)
    1.62 +          nodup_depth_tac cs' n;	(* slower but more general *)
    1.63      in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
    1.64  	       TRY (Classical.safe_tac cs),
    1.65  	       REPEAT (FIRSTGOAL maintac),