src/HOL/Tools/Metis/metis_reconstruct.ML

 fun atp_name_from_metis s =
   case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)
 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
-    let val (s, swap) = atp_name_from_metis s in
+    let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
     end
-  | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
+  | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
 
 fun hol_term_from_metis ctxt sym_tab =
   atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
 
 fun atp_literal_from_metis (pos, atom) =

              | TYPE _ =>
                (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
                                          " in " ^ Display.string_of_thm ctxt i_th);
                 NONE)
       fun remove_typeinst (a, t) =
-            case strip_prefix_and_unascii schematic_var_prefix a of
-                SOME b => SOME (b, t)
-              | NONE => case strip_prefix_and_unascii tvar_prefix a of
-                SOME _ => NONE          (*type instantiations are forbidden!*)
-              | NONE => SOME (a,t)    (*internal Metis var?*)
+        let val a = Metis_Name.toString a in
+          case strip_prefix_and_unascii schematic_var_prefix a of
+            SOME b => SOME (b, t)
+          | NONE =>
+            case strip_prefix_and_unascii tvar_prefix a of
+              SOME _ => NONE (* type instantiations are forbidden *)
+            | NONE => SOME (a, t) (* internal Metis var? *)
+        end
       val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
       val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
       val (vars, tms) =
         ListPair.unzip (map_filter subst_translation substs)
         ||> reveal_old_skolems_and_infer_types ctxt old_skolems

                         SOME t => " fol-term: " ^ Metis_Term.toString t
                       | NONE => ""))
       fun path_finder tm [] _ = (tm, Bound 0)
         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
           let
-            val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
+            val s = s |> Metis_Name.toString
+                      |> perhaps (try (strip_prefix_and_unascii const_prefix
                                        #> the #> unmangled_const_name))
           in
             if s = metis_predicator orelse s = predicator_name orelse
                s = metis_type_tag orelse s = type_tag_name then
               path_finder tm ps (nth ts p)

             val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
         in  th'  end
         handle THM _ => th;
 
-fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
+fun is_metis_literal_genuine (_, (s, _)) =
+  not (String.isPrefix class_prefix (Metis_Name.toString s))
 fun is_isabelle_literal_genuine t =
   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0