--- a/src/Tools/Code/code_runtime.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon May 30 20:58:54 2016 +0200
@@ -549,7 +549,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)))]))