--- 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 =