src/HOL/Tools/inductive_realizer.ML
changeset 28328 9a647179c1e6
parent 28083 103d9282a946
child 28800 48f7bfebd31d
     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