diff -r f5f726ef4f6a -r 7497ff20f1e8 src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jul 25 08:32:32 2011 +0200
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Jul 26 13:27:59 2011 +0200
@@ -12,7 +12,7 @@
   Diophant'_equation :: "[bool, int, bool ] 
                                        => bool "
                     ("((Script Diophant'_equation (_ _ =))//(_))" 9)
-axioms
+axiomatization where
 
   int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"