# HG changeset patch
# User wenzelm
# Date 1136062176 -3600
# Node ID 540da24157515d9996da03a6fe19252c3a8b88ef
# Parent  85e7f80023fc23bb8231fdbb7504d0373bfeca7a
removed obsolete Provers/make_elim.ML;

diff -r 85e7f80023fc -r 540da2415751 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/IsaMakefile	Sat Dec 31 21:49:36 2005 +0100
@@ -32,9 +32,9 @@
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
   $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML			\
-  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/project_rule.ML            \
-  $(SRC)/Provers/quantifier1.ML	$(SRC)/Provers/splitter.ML FOL.ML FOL.thy \
-  FOL_lemmas1.ML IFOL.ML IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \
+  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
+  $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML	\
+  IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML 		\
   document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML	\
   intprover.ML simpdata.ML
 	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
diff -r 85e7f80023fc -r 540da2415751 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/ROOT.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -12,7 +12,6 @@
 use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";
-use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";
 use "~~/src/Provers/clasimp.ML";
diff -r 85e7f80023fc -r 540da2415751 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/cladata.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -8,17 +8,9 @@
 
 section "Classical Reasoner";
 
-(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
-
-(*we don't redeclare the original make_elim (Tactic.make_elim) for 
-  compatibility 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 make_elim = cla_make_elim
   val mp        = mp
   val not_elim  = notE
   val classical = classical
diff -r 85e7f80023fc -r 540da2415751 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -369,8 +369,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Cla and Blast = Blast
-  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
-  val cla_make_elim = cla_make_elim);
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);
diff -r 85e7f80023fc -r 540da2415751 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/IsaMakefile	Sat Dec 31 21:49:36 2005 +0100
@@ -71,8 +71,8 @@
   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
-  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML			\
-  $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
+  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
+  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
   $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
   $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
diff -r 85e7f80023fc -r 540da2415751 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/ROOT.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -14,7 +14,6 @@
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";
-use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";
 use "~~/src/Provers/clasimp.ML";
diff -r 85e7f80023fc -r 540da2415751 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/cladata.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -36,18 +36,9 @@
     (List.nth (Thm.prems_of thm, i - 1)) then hyp_subst_tac i thm else no_tac thm;
 
 
-
-(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
-
-(*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 make_elim = cla_make_elim
   val mp        = mp
   val not_elim  = notE
   val classical = classical
diff -r 85e7f80023fc -r 540da2415751 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -433,8 +433,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
-  val cla_make_elim = cla_make_elim);
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
 open Clasimp;
 
 val HOL_css = (HOL_cs, HOL_ss);
diff -r 85e7f80023fc -r 540da2415751 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/Provers/clasimp.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -18,7 +18,6 @@
   val notE: thm
   val iffD1: thm
   val iffD2: thm
-  val cla_make_elim: thm -> thm
 end
 
 signature CLASIMP =
@@ -140,7 +139,7 @@
     val zero_rotate = zero_var_indexes o rotate_prems n;
   in
     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
-           [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
+           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
       handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
@@ -149,7 +148,7 @@
 fun delIff delcs delss ((cs, ss), th) =
   let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
     (delcs (cs, [zero_rotate (th RS Data.iffD2),
-        Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
+        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
       handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
         handle THM _ => delcs (cs, [th])),
      delss (ss, [th]))