--- a/src/FOL/cladata.ML Tue Sep 05 18:43:05 2000 +0200
+++ b/src/FOL/cladata.ML Tue Sep 05 18:43:22 2000 +0200
@@ -9,12 +9,7 @@
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);
+structure Make_Elim = Make_Elim_Fun(val classical = classical);
(*we don't redeclare the original make_elim (Tactic.make_elim) for
compatibliity with strange things done in many existing proofs *)