equal
deleted
inserted
replaced
14 struct |
14 struct |
15 |
15 |
16 (***** construct a theorem out of a proof term *****) |
16 (***** construct a theorem out of a proof term *****) |
17 |
17 |
18 fun lookup_thm thy = |
18 fun lookup_thm thy = |
19 let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in |
19 let |
20 fn s => |
20 val tab = |
21 (case Symtab.lookup tab s of |
21 Thm_Name.Table.build (Global_Theory.all_thms_of thy true |> fold_rev Thm_Name.Table.update); |
22 NONE => error ("Unknown theorem " ^ quote s) |
22 in |
|
23 fn name => |
|
24 (case Thm_Name.Table.lookup tab name of |
|
25 NONE => error ("Unknown theorem " ^ quote (Thm_Name.print name)) |
23 | SOME thm => thm) |
26 | SOME thm => thm) |
24 end; |
27 end; |
25 |
28 |
26 val beta_eta_convert = |
29 val beta_eta_convert = |
27 Conv.fconv_rule Drule.beta_eta_conversion; |
30 Conv.fconv_rule Drule.beta_eta_conversion; |
85 (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) |
88 (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) |
86 end; |
89 end; |
87 |
90 |
88 fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) = |
91 fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) = |
89 let |
92 let |
90 val name = Thm_Name.short thm_name; |
93 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name)); |
91 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); |
|
92 val prop = Thm.prop_of thm; |
94 val prop = Thm.prop_of thm; |
93 val _ = |
95 val _ = |
94 if is_equal prop prop' then () |
96 if is_equal prop prop' then () |
95 else |
97 else |
96 error ("Duplicate use of theorem name " ^ |
98 error ("Duplicate use of theorem name " ^ |