--- a/src/HOL/Tools/record_package.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Wed Apr 04 23:29:33 2007 +0200
@@ -1703,10 +1703,10 @@
fun meta_to_obj_all thm =
let
- val {sign, prop, ...} = rep_thm thm;
+ val {thy, prop, ...} = rep_thm thm;
val params = Logic.strip_params prop;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
- val ct = cterm_of sign
+ val ct = cterm_of thy
(HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
in