diff -r eb8a3a991c08 -r c59c471126ab ROOT.ML
--- a/ROOT.ML	Sun Nov 06 21:04:50 1994 +0100
+++ b/ROOT.ML	Tue Nov 08 11:21:33 1994 +0100
@@ -30,13 +30,7 @@
   struct
   (*Take apart an equality judgement; otherwise raise Match!*)
   fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
-
   val imp_intr = impI
-
-  (*etac rev_cut_eq moves an equality to be the last premise. *)
-  val rev_cut_eq = prove_goal HOL.thy "[| a=b;  a=b ==> R |] ==> R"
-   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
-
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
@@ -45,13 +39,13 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
-(** Applying ClassicalFun to create a classical prover **)
-structure Classical_Data =
+(*** Applying ClassicalFun to create a classical prover ***)
+structure Classical_Data = 
   struct
-  val sizef = size_of_thm
-  val mp = mp
-  val not_elim = notE
-  val classical = classical
+  val sizef	= size_of_thm
+  val mp	= mp
+  val not_elim	= notE
+  val classical	= classical
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
 
@@ -66,9 +60,6 @@
 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,ex1E] addEs [allE];
 
-val HOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
-                         addSEs [exE,ex1E] addEs [all_dupE];
-
 structure HOL_Induction = InductionFun(struct val spec=spec end);
 open HOL_Induction;