src/HOL/Tools/Metis/metis_reconstruct.ML

             SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =
             case strip_prefix_and_unascii const_prefix a of
                 SOME b =>
                   let
-                    val c = invert_const b
+                    val c = b |> invert_const |> unproxify_const
                     val ntypes = num_type_args thy c
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
                     val tys = types_of (List.take(tts,ntypes))
                     val t =

 (*Maps fully-typed metis terms to isabelle terms*)
 fun hol_term_from_metis_FT ctxt fol_tm =
   let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
                                        Metis_Term.toString fol_tm)
       fun do_const c =
-        let val c = c |> invert_const in
+        let val c = c |> invert_const |> unproxify_const in
           if String.isPrefix new_skolem_const_prefix c then
             Var ((new_skolem_var_name_from_const c, 1), dummyT)
           else
             Const (c, dummyT)
         end