src/FOLP/FOLP.thy
changeset 42799 4e33894aec6d
parent 41779 a68f503805ed
child 48891 c0eafbd55de3
--- a/src/FOLP/FOLP.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOLP/FOLP.thy	Sat May 14 11:42:43 2011 +0200
@@ -103,17 +103,14 @@
 use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
 
 ML {*
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
-struct
+structure Cla = Classical
+(
   val sizef = size_of_thm
   val mp = @{thm mp}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val hyp_subst_tacs = [hyp_subst_tac]
-end;
-
-structure Cla = ClassicalFun(Classical_Data);
+);
 open Cla;
 
 (*Propositional rules