--- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 04 23:29:33 2007 +0200
@@ -64,8 +64,8 @@
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
fun prf_of thm =
- let val {sign, prop, der = (_, prf), ...} = rep_thm thm
- in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
+ let val {thy, prop, der = (_, prf), ...} = rep_thm thm
+ in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)