src/HOL/Tools/record_package.ML

     val th2 = Drule.forall_intr_vars th1;
   in th2 end;
 
 fun meta_to_obj_all thm =
   let
-    val {thy, prop, ...} = rep_thm thm;
+    val thy = Thm.theory_of_thm thm;
+    val prop = Thm.prop_of thm;
     val params = Logic.strip_params prop;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
     val ct = cterm_of thy
       (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
     val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));