src/ZF/Coind/Static.thy

--- a/src/ZF/Coind/Static.thy	Fri Feb 18 16:36:42 2011 +0100
+++ b/src/ZF/Coind/Static.thy	Fri Feb 18 17:03:30 2011 +0100
@@ -9,11 +9,8 @@
      parameter of the proof.  A concrete version could be defined inductively.
 ***)
 
-consts
-  isof :: "[i,i] => o"
-
-axioms
-  isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+axiomatization isof :: "[i,i] => o"
+  where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
 
 (*Its extension to environments*)