diff -r 5f79a9e42507 -r a68f503805ed src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Fri Feb 18 16:36:42 2011 +0100
+++ b/src/FOLP/FOLP.thy	Fri Feb 18 17:03:30 2011 +0100
@@ -11,10 +11,8 @@
   ("classical.ML") ("simp.ML") ("simpdata.ML")
 begin
 
-consts
-  cla :: "[p=>p]=>p"
-axioms
-  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axiomatization cla :: "[p=>p]=>p"
+  where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
 
 
 (*** Classical introduction rules for | and EX ***)