equal
deleted
inserted
replaced
15 structure InductiveRealizer : INDUCTIVE_REALIZER = |
15 structure InductiveRealizer : INDUCTIVE_REALIZER = |
16 struct |
16 struct |
17 |
17 |
18 (* FIXME: LocalTheory.note should return theorems with proper names! *) |
18 (* FIXME: LocalTheory.note should return theorems with proper names! *) |
19 fun name_of_thm thm = |
19 fun name_of_thm thm = |
20 (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of |
20 (case Symtab.dest (Proofterm.thms_of_proof' (Thm.proof_of thm) Symtab.empty) of |
21 [(name, _)] => name |
21 [(name, _)] => name |
22 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); |
22 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); |
23 |
23 |
24 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); |
24 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); |
25 |
25 |