src/FOL/cladata.ML
changeset 18522 9bdfb6eaf8ab
parent 17876 b9c92f384109
child 18529 540da2415751
--- a/src/FOL/cladata.ML	Fri Dec 30 16:56:54 2005 +0100
+++ b/src/FOL/cladata.ML	Fri Dec 30 16:56:56 2005 +0100
@@ -9,7 +9,7 @@
 section "Classical Reasoner";
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun(val classical = classical);
+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 *)