# HG changeset patch
# User wenzelm
# Date 1222177730 -7200
# Node ID 9a647179c1e65de3048ef4c95287a435a8422398
# Parent  4d7a0a941b79dece3dc880d6cdab9d656b9a69eb
Thm.proof_of;

diff -r 4d7a0a941b79 -r 9a647179c1e6 src/HOL/Tools/inductive_realizer.ML
--- 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));