# HG changeset patch
# User wenzelm
# Date 1226781079 -3600
# Node ID 48f7bfebd31d61f1eb8ed3fb1492b1ce0830d2b4
# Parent  ee65e7d043fcda05452093d260fc2fe6f466354a
name_of_thm: Proofterm.fold_proof_atoms;
Thm.proof_of returns proof_body;

diff -r ee65e7d043fc -r 48f7bfebd31d src/HOL/Tools/inductive_realizer.ML
--- 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 =