src/HOL/Matrix/cplex/matrixlp.ML

 structure MatrixLP : MATRIX_LP =
 struct
 
 fun inst_real thm =
   let val certT = ctyp_of (Thm.theory_of_thm thm) in
-    Drule.standard (Thm.instantiate
+    Drule.export_without_context (Thm.instantiate
       ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
   end
 
 local
 

     let
         val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
         val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
         val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
     in
-        Drule.standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
+        Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
     end
 
 fun inst_tvars [] thms = thms
   | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)