diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 02 13:55:43 2015 +0200
@@ -171,11 +171,10 @@
 (* INFERENCE RULE: RESOLVE *)
 
 (*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
+fun incr_type_indexes ctxt inc th =
   let
     val tvs = Term.add_tvars (Thm.full_prop_of th) []
-    val thy = Thm.theory_of_thm th
-    fun inc_tvar ((a, i), s) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
+    fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
   in
     Thm.instantiate (map inc_tvar tvs, []) th
   end
@@ -185,7 +184,7 @@
    Instantiations of those Vars could then fail. *)
 fun resolve_inc_tyvars ctxt tha i thb =
   let
-    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
+    val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
             (false, tha, Thm.nprems_of tha) i thb
@@ -393,16 +392,16 @@
   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
     equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
 
-fun flexflex_first_order th =
+fun flexflex_first_order ctxt th =
   (case Thm.tpairs_of th of
     [] => th
   | pairs =>
       let
-        val thy = Thm.theory_of_thm th
+        val thy = Proof_Context.theory_of ctxt
         val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   
-        fun mkT (v, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (v, S), T)
-        fun mk (v, (T, t)) = apply2 (Thm.global_cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
+        fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
   
         val instsT = Vartab.fold (cons o mkT) tyenv []
         val insts = Vartab.fold (cons o mk) tenv []
@@ -462,7 +461,7 @@
       val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
       val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
       val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
-        |> flexflex_first_order
+        |> flexflex_first_order ctxt
         |> resynchronize ctxt fol_th
       val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
       val _ = trace_msg ctxt (fn () => "=============================================")