diff -r 6c05c4632949 -r b9e1d53124f5 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat May 28 17:35:12 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sat May 28 21:38:58 2016 +0200
@@ -548,7 +548,7 @@
 fun add_definiendum (ml_name, (b, T)) thy =
   thy
   |> Code_Target.add_reserved target ml_name
-  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
+  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))