diff -r ca3f7bb866f3 -r 463c9e9111ae src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -18,7 +18,7 @@
 (* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
 fun name_of_thm thm =
   (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
-      [Proofterm.proof_of (Thm.proof_of thm)] [] of
+      [Thm.proof_of thm] [] of
     [name] => name
   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
 
@@ -27,8 +27,7 @@
 fun prf_of thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val thm' =
-      Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm));
+    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
   in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
 
 fun forall_intr_prf t prf =