src/HOL/Tools/datatype_realizer.ML

                     (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
                 end
             | _ => AbsP ("H", SOME p, prf)))
           (rec_fns ~~ Thm.prems_of thm)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
       else
         Logic.varify_global (fold_rev lambda

         (fold_rev (fn (p, r) => fn prf =>
             Proofterm.forall_intr_proof' (Logic.varify_global r)
               (AbsP ("H", SOME (Logic.varify_global p), prf)))
           (prems ~~ rs)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
     val prf' =
       Extraction.abs_corr_shyps thy' exhaust []
-        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
         (fold_rev (Term.abs o dest_Free) rs
           (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
   in