src/Pure/Proof/extraction.ML

           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
           val env' = Envir.Envir
             {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
              tenv = tenv, tyenv = Tenv};
-          val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
+          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
         in SOME (Envir.norm_term env'' (inc (ren tm2)))
         end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
           (sort (int_ord o pairself fst)
             (Net.match_term rules (Envir.eta_contract tm)))
       end;