diff -r 73dc3b2a7102 -r 2fc3f4450fe8 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Sep 11 16:32:31 1998 +0200
+++ b/src/Provers/clasimp.ML	Fri Sep 11 17:20:58 1998 +0200
@@ -38,15 +38,17 @@
   val delsimps2	: clasimpset * thm list -> clasimpset
   val addSss	: claset * simpset -> claset
   val addss	: claset * simpset -> claset
-  val CLASIMPSET: (clasimpset -> tactic) -> tactic
-  val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
-  val mk_auto_tac:clasimpset -> int -> int -> tactic
-  val auto_tac	: clasimpset -> tactic
-  val Auto_tac	: tactic
-  val auto	: unit -> unit
-  val force_tac	: clasimpset  -> int -> tactic
-  val Force_tac	: int -> tactic
-  val force	: int -> unit
+  val CLASIMPSET  :(clasimpset -> tactic) -> tactic
+  val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
+  val clarsimp_tac: clasimpset -> int -> tactic
+  val Clarsimp_tac:               int -> tactic
+  val mk_auto_tac : clasimpset -> int -> int -> tactic
+  val auto_tac	  : clasimpset -> tactic
+  val Auto_tac	  : tactic
+  val auto	  : unit -> unit
+  val force_tac	  : clasimpset  -> int -> tactic
+  val Force_tac	  : int -> tactic
+  val force	  : int -> unit
 end;
 
 functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
@@ -82,8 +84,8 @@
 (*Caution: only one simpset added can be added by each of addSss and addss*)
 fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
 			CHANGED o Simplifier.safe_asm_full_simp_tac ss);
-fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", Simplifier.asm_full_simp_tac ss);
-
+fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", 
+				  Simplifier.asm_full_simp_tac ss);
 
 (* tacticals *)
 
@@ -94,6 +96,11 @@
   Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
 
 
+fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_MAYBE'
+			    Classical.clarify_tac (cs addSss ss);
+fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
+
+
 (* auto_tac *)
 
 fun blast_depth_tac cs m i thm =