Thm.proof_of;

--- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 22 23:04:35 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Sep 23 15:48:50 2008 +0200
@@ -17,7 +17,7 @@
 
 (* FIXME: LocalTheory.note should return theorems with proper names! *)
 fun name_of_thm thm =
-  (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
+  (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));