--- a/src/HOL/Tools/inductive_realizer.ML Sat Nov 15 21:31:17 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Nov 15 21:31:19 2008 +0100
@@ -15,18 +15,20 @@
structure InductiveRealizer : INDUCTIVE_REALIZER =
struct
-(* FIXME: LocalTheory.note should return theorems with proper names! *)
+(* FIXME: LocalTheory.note should return theorems with proper names! *) (* FIXME ?? *)
fun name_of_thm thm =
- (case Symtab.dest (Proofterm.thms_of_proof' (Thm.proof_of thm) Symtab.empty) of
- [(name, _)] => name
- | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
+ (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
+ [Proofterm.proof_of (Thm.proof_of thm)] [] of
+ [name] => name
+ | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
fun prf_of thm =
let
val thy = Thm.theory_of_thm thm;
- val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
+ val thm' =
+ Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm));
in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
fun forall_intr_prf t prf =