src/Tools/Code/code_runtime.ML

 end;
 
 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)))]))
   #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated []));