equal
deleted
inserted
replaced
546 end; |
546 end; |
547 |
547 |
548 fun add_definiendum (ml_name, (b, T)) thy = |
548 fun add_definiendum (ml_name, (b, T)) thy = |
549 thy |
549 thy |
550 |> Code_Target.add_reserved target ml_name |
550 |> Code_Target.add_reserved target ml_name |
551 |> Specification.axiomatization [(b, SOME T, NoSyn)] [] |
551 |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] |
552 |-> (fn ([Const (const, _)], _) => |
552 |-> (fn ([Const (const, _)], _) => |
553 Code_Target.set_printings (Constant (const, |
553 Code_Target.set_printings (Constant (const, |
554 [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) |
554 [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) |
555 #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated [])); |
555 #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated [])); |
556 |
556 |