src/HOL/Import/proof_kernel.ML

         quote(
         PrintMode.setmp [] (
         Library.setmp show_brackets false (
         Library.setmp show_all_types true (
         Library.setmp Syntax.ambiguity_is_error false (
-        Library.setmp show_sorts true string_of_cterm))))
+        Library.setmp show_sorts true Display.string_of_cterm))))
         ct)
     end
 
 exception SMART_STRING
 

           | G 2 = Library.setmp show_all_types true (G 0)
           | G 3 = Library.setmp show_brackets true (G 2)
           | G _ = raise SMART_STRING
         fun F n =
             let
-                val str = Library.setmp show_brackets false (G n string_of_cterm) ct
+                val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
                 val u = Syntax.parse_term ctxt str
                   |> TypeInfer.constrain T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str
                 else F (n+1)
             end
             handle ERROR mesg => F (n+1)
-                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
+                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     in
       PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
     end
     handle ERROR mesg => simple_smart_string_of_cterm ct
 
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
-fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
-fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
+fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
+fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
 fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
         (*val _ = writeln "Renaming:"
         val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)

         val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
         val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
                     then
                         let
                             val p1 = quotename constname
-                            val p2 = string_of_ctyp (ctyp_of thy'' ctype)
+                            val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
                             val p3 = string_of_mixfix csyn
                             val p4 = smart_string_of_cterm crhs
                         in
                             add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
                         end
                     else
-                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
+                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
                                    "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
                                   thy'')
         val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
                       SOME (_,res) => HOLThm(rens_of linfo,res)
                     | NONE => raise ERR "new_definition" "Bad conclusion"

                                                               val (_,cT,p) = dest_exists ex
                                                           in
                                                               ((cname,cT,mk_syn thy cname)::cs,p)
                                                           end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
                                val str = Library.foldl (fn (acc,(c,T,csyn)) =>
-                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
+                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
                                val thy' = add_dump str thy
                                val _ = ImportRecorder.add_consts consts
                            in
                                Sign.add_consts_i consts thy'
                            end

         handle e => (message "exception in new_type_definition"; print_exn e)
 
 fun add_dump_constdefs thy defname constname rhs ty =
     let
         val n = quotename constname
-        val t = string_of_ctyp (ctyp_of thy ty)
+        val t = Display.string_of_ctyp (ctyp_of thy ty)
         val syn = string_of_mixfix (mk_syn thy constname)
         (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
         val eq = quote (constname ^ " == "^rhs)
         val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
     in

               (string_of_mixfix tsyn) ^ " morphisms "^
               (quote rep_name)^" "^(quote abs_name)^"\n"^
               ("  apply (rule light_ex_imp_nonempty[where t="^
               (proc_prop (cterm_of thy4 t))^"])\n"^
               ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
-            val str_aty = string_of_ctyp (ctyp_of thy aty)
+            val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
             val thy = add_dump_syntax thy rep_name
             val thy = add_dump_syntax thy abs_name
             val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
               " = typedef_hol2hollight \n"^
               "  [where a=\"a :: "^str_aty^"\" and r=r" ^