equal
deleted
inserted
replaced
46 |
46 |
47 fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => |
47 fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => |
48 let |
48 let |
49 val {intros, graph, eqns} = CodegenData.get thy; |
49 val {intros, graph, eqns} = CodegenData.get thy; |
50 fun thyname_of s = (case optmod of |
50 fun thyname_of s = (case optmod of |
51 NONE => thyname_of_const s thy | SOME s => s); |
51 NONE => Codegen.thyname_of_const thy s | SOME s => s); |
52 in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of |
52 in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of |
53 SOME (Const ("op =", _), [t, _]) => (case head_of t of |
53 SOME (Const ("op =", _), [t, _]) => (case head_of t of |
54 Const (s, _) => |
54 Const (s, _) => |
55 CodegenData.put {intros = intros, graph = graph, |
55 CodegenData.put {intros = intros, graph = graph, |
56 eqns = eqns |> Symtab.map_default (s, []) |
56 eqns = eqns |> Symtab.map_default (s, []) |
83 let val {intros, graph, ...} = CodegenData.get thy |
83 let val {intros, graph, ...} = CodegenData.get thy |
84 in case Symtab.lookup intros s of |
84 in case Symtab.lookup intros s of |
85 NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of |
85 NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of |
86 NONE => NONE |
86 NONE => NONE |
87 | SOME ({names, ...}, {intrs, raw_induct, ...}) => |
87 | SOME ({names, ...}, {intrs, raw_induct, ...}) => |
88 SOME (names, thyname_of_const s thy, |
88 SOME (names, Codegen.thyname_of_const thy s, |
89 length (InductivePackage.params_of raw_induct), |
89 length (InductivePackage.params_of raw_induct), |
90 preprocess thy intrs)) |
90 preprocess thy intrs)) |
91 | SOME _ => |
91 | SOME _ => |
92 let |
92 let |
93 val SOME names = find_first |
93 val SOME names = find_first |