src/HOL/Tools/Nitpick/nitpick_model.ML

             make_plain_fun maybe_opt T1 T2
             #> unarize_unbox_etc_term
             #> format_fun (uniterize_unarize_unbox_etc_type T')
                           (uniterize_unarize_unbox_etc_type T1)
                           (uniterize_unarize_unbox_etc_type T2))
-
 
     fun term_for_fun_or_set seen T T' j =
         let
           val k1 = card_of_type card_assigns (pseudo_domain_type T)
           val k2 = card_of_type card_assigns (pseudo_range_type T)

         end
       else
         t1 = t2
     end
 
+fun pretty_term_auto_global ctxt t =
+  let
+    fun add_fake_const s =
+      Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
+      #> #2
+
+    val globals = Term.add_const_names t []
+      |> filter_out (String.isSubstring Long_Name.separator)
+
+    val fake_ctxt =
+      ctxt |> Proof_Context.background_theory (fn thy =>
+        thy
+        |> Sign.map_naming (K Name_Space.global_naming)
+        |> fold (perhaps o try o add_fake_const) globals
+        |> Sign.restore_naming thy)
+  in
+    Syntax.pretty_term fake_ctxt t
+  end
+
 fun reconstruct_hol_model {show_types, show_skolems, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
                       debug, whacks, binary_ints, destroy_constrs, specialize,
                       star_linear_preds, total_consts, needs, tac_timeout,
                       evals, case_names, def_tables, nondef_table, nondefs,

                       card_assigns, bits, bisim_depth, data_types, ofs} : scope)
         formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
         rel_table bounds =
   let
     val pool = Unsynchronized.ref []
-    val (wacky_names as (_, base_step_names), ctxt) =
-      add_wacky_syntax ctxt
+    val (wacky_names as (_, base_step_names), ctxt) = add_wacky_syntax ctxt
     val hol_ctxt =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
        binary_ints = binary_ints, destroy_constrs = destroy_constrs,
        specialize = specialize, star_linear_preds = star_linear_preds,

                    tuple_list_for_name rel_table bounds name
                    |> term_for_rep (not (is_fully_representable_set name)) false
                                    T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
-            [Syntax.pretty_term ctxt t1, Pretty.str oper,
-             Syntax.pretty_term ctxt t2])
+            [pretty_term_auto_global ctxt t1, Pretty.str oper,
+             pretty_term_auto_global ctxt t2])
       end
     fun pretty_for_data_type ({typ, card, complete, ...} : data_type_spec) =
       Pretty.block (Pretty.breaks
           (pretty_for_type ctxt typ ::
            (case typ of
               Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
             | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
             | _ => []) @
            [Pretty.str "=",
             Pretty.enum "," "{" "}"
-                (map (Syntax.pretty_term ctxt) (all_values card typ) @
+                (map (pretty_term_auto_global ctxt) (all_values card typ) @
                  (if fun_from_pair complete false then []
                   else [Pretty.str (unrep ())]))]))
     fun integer_data_type T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
         self_rec = true, complete = (false, false), concrete = (true, true),