equal
deleted
inserted
replaced
20 (** add_constdefs(_i) **) |
20 (** add_constdefs(_i) **) |
21 |
21 |
22 fun gen_constdef prep_vars prep_prop prep_att |
22 fun gen_constdef prep_vars prep_prop prep_att |
23 structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy = |
23 structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy = |
24 let |
24 let |
25 val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead"); |
25 val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead"; |
26 |
26 |
27 fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); |
27 fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); |
28 |
28 |
29 val thy_ctxt = ProofContext.init_global thy; |
29 val thy_ctxt = ProofContext.init_global thy; |
30 val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt); |
30 val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt); |