1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 22 23:04:35 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Sep 23 15:48:50 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  (* FIXME: LocalTheory.note should return theorems with proper names! *)
     1.6  fun name_of_thm thm =
     1.7 -  (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
     1.8 +  (case Symtab.dest (Proofterm.thms_of_proof' (Thm.proof_of thm) Symtab.empty) of
     1.9       [(name, _)] => name
    1.10     | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    1.11