--- a/src/Tools/Code/code_runtime.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Apr 28 09:43:11 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)))]))