equal
deleted
inserted
replaced
12 |
12 |
13 structure InductiveRealizer : INDUCTIVE_REALIZER = |
13 structure InductiveRealizer : INDUCTIVE_REALIZER = |
14 struct |
14 struct |
15 |
15 |
16 fun name_of_thm thm = |
16 fun name_of_thm thm = |
17 (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _, _), _)) => cons name | _ => I) |
17 (case Proofterm.fold_proof_atoms false (fn PThm ({name, ...}, _) => cons name | _ => I) |
18 [Thm.proof_of thm] [] of |
18 [Thm.proof_of thm] [] of |
19 [name] => name |
19 [name] => name |
20 | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); |
20 | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); |
21 |
21 |
22 fun prf_of thy raw_thm = |
22 fun prf_of thy raw_thm = |