--- 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