src/FOL/simpdata.ML

 
 simpset_ref() := FOL_ss;
 
 
 
-
-
-
-
-(*** Integration of simplifier with classical reasoner ***)
+(*** integration of simplifier with classical reasoner ***)
 
 (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    fails if there is no equaliy or if an equality is already at the front *)
 local
   fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true

 val rot_eq_tac = 
      SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
 		if n>0 then rotate_tac n i else no_tac end)
 end;
 
-use "$ISABELLE_HOME/src/Provers/clasimp.ML";
+
+structure Clasimp = ClasimpFun
+ (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
+  val addcongs = op addcongs and delcongs = op delcongs
+  and addSaltern = op addSaltern and addbefore = op addbefore);
+
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);
-