declaring and using cla_make_elim

--- a/src/FOL/cladata.ML	Wed Jun 28 10:37:08 2000 +0200
+++ b/src/FOL/cladata.ML	Wed Jun 28 10:37:52 2000 +0200
@@ -8,14 +8,26 @@
 
 section "Classical Reasoner";
 
+(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
+structure Make_Elim_Data =
+struct
+  val classical = classical
+end;
+
+structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+
+(*we don't redeclare the original make_elim (Tactic.make_elim) for 
+  compatibliity with strange things done in many existing proofs *)
+val cla_make_elim = Make_Elim.make_elim;
 
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
-  val sizef     = size_of_thm
+  val make_elim = cla_make_elim
   val mp        = mp
   val not_elim  = notE
   val classical = classical
+  val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
 

--- a/src/HOL/cladata.ML	Wed Jun 28 10:37:08 2000 +0200
+++ b/src/HOL/cladata.ML	Wed Jun 28 10:37:52 2000 +0200
@@ -29,13 +29,27 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
+
+(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
+structure Make_Elim_Data =
+struct
+  val classical = classical
+end;
+
+structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+
+(*we don't redeclare the original make_elim (Tactic.make_elim) for 
+  compatibliity with strange things done in many existing proofs *)
+val cla_make_elim = Make_Elim.make_elim;
+
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
-  val sizef     = size_of_thm
+  val make_elim = cla_make_elim
   val mp        = mp
   val not_elim  = notE
   val classical = classical
+  val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
   end;