src/Tools/Code/code_runtime.ML
changeset 63064 2f18172214c8
parent 62902 3c0f53eae166
child 63156 3cb84e4469a7
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Apr 27 10:03:35 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Apr 28 09:43:11 2016 +0200
     1.3 @@ -548,7 +548,7 @@
     1.4  fun add_definiendum (ml_name, (b, T)) thy =
     1.5    thy
     1.6    |> Code_Target.add_reserved target ml_name
     1.7 -  |> Specification.axiomatization [(b, SOME T, NoSyn)] []
     1.8 +  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
     1.9    |-> (fn ([Const (const, _)], _) =>
    1.10      Code_Target.set_printings (Constant (const,
    1.11        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))