src/Tools/Code/code_runtime.ML
changeset 63184 dd6cd88cebd9
parent 63174 57c0d60e491c
parent 63178 b9e1d53124f5
child 64928 18a6b96f8b00
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sun May 29 14:43:18 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon May 30 20:58:54 2016 +0200
     1.3 @@ -549,7 +549,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)))]))