equal
deleted
inserted
replaced
15 -> (Attrib.binding * (thm list * Args.src list) list) list |
15 -> (Attrib.binding * (thm list * Args.src list) list) list |
16 -> (Attrib.binding * (thm list * Args.src list) list) list |
16 -> (Attrib.binding * (thm list * Args.src list) list) list |
17 -> local_theory -> local_theory) |
17 -> local_theory -> local_theory) |
18 -> string -> (Attrib.binding * (thm list * Args.src list) list) list |
18 -> string -> (Attrib.binding * (thm list * Args.src list) list) list |
19 -> local_theory -> (string * thm list) list * local_theory |
19 -> local_theory -> (string * thm list) list * local_theory |
20 val abbrev: (string * bool -> binding * mixfix -> term * term -> (string * sort) list * term list |
20 val abbrev: (string * bool -> binding * mixfix -> term * term |
21 -> local_theory -> local_theory) |
21 -> (string * sort) list * term list -> local_theory -> local_theory) |
22 -> string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory |
22 -> string * bool -> (binding * mixfix) * term -> local_theory |
|
23 -> (term * term) * local_theory |
23 end; |
24 end; |
24 |
25 |
25 structure Generic_Target: GENERIC_TARGET = |
26 structure Generic_Target: GENERIC_TARGET = |
26 struct |
27 struct |
27 |
28 |
83 val cert = Thm.cterm_of thy; |
84 val cert = Thm.cterm_of thy; |
84 |
85 |
85 (*export assumes/defines*) |
86 (*export assumes/defines*) |
86 val th = Goal.norm_result raw_th; |
87 val th = Goal.norm_result raw_th; |
87 val (defs, th') = Local_Defs.export ctxt thy_ctxt th; |
88 val (defs, th') = Local_Defs.export ctxt thy_ctxt th; |
88 val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt); |
89 val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) |
|
90 (Assumption.all_assms_of ctxt); |
89 val nprems = Thm.nprems_of th' - Thm.nprems_of th; |
91 val nprems = Thm.nprems_of th' - Thm.nprems_of th; |
90 |
92 |
91 (*export fixes*) |
93 (*export fixes*) |
92 val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
94 val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
93 val frees = map Free (Thm.fold_terms Term.add_frees th' []); |
95 val frees = map Free (Thm.fold_terms Term.add_frees th' []); |