src/HOL/Tools/Lifting/lifting_setup.ML

     val _ = 
       if (Thm.nprems_of quot_thm > 0) then   
           raise QUOT_ERROR [Pretty.block
             [Pretty.str "The Quotient theorem has extra assumptions:",
              Pretty.brk 1,
-             Display.pretty_thm ctxt quot_thm]]
+             Thm.pretty_thm ctxt quot_thm]]
       else ()
     val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
     handle TERM _ => raise QUOT_ERROR
           [Pretty.block
             [Pretty.str "The Quotient theorem is not of the right form:",
              Pretty.brk 1,
-             Display.pretty_thm ctxt quot_thm]]
+             Thm.pretty_thm ctxt quot_thm]]
     val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
     val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
     val rty_tfreesT = Term.add_tfree_namesT rty []
     val qty_tfreesT = Term.add_tfree_namesT qty []
     val extra_rty_tfrees =

             val pcr_cr_eq = #pcr_cr_eq pcr
             val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def)
               handle TERM _ => raise PCR_ERROR [Pretty.block 
                     [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
                     Pretty.brk 1,
-                    Display.pretty_thm ctxt pcrel_def]]
+                    Thm.pretty_thm ctxt pcrel_def]]
             val pcr_const_def = head_of def_lhs
             val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
               handle TERM _ => raise PCR_ERROR [Pretty.block 
                     [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
                     Pretty.brk 1,
-                    Display.pretty_thm ctxt pcr_cr_eq]]
+                    Thm.pretty_thm ctxt pcr_cr_eq]]
             val (pcr_const_eq, eqs) = strip_comb eq_lhs
             fun is_eq (Const (@{const_name HOL.eq}, _)) = true
               | is_eq _ = false
             fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
               | eq_Const _ _ = false
             val all_eqs = if not (forall is_eq eqs) then 
               [Pretty.block
                     [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
                     Pretty.brk 1,
-                    Display.pretty_thm ctxt pcr_cr_eq]]
+                    Thm.pretty_thm ctxt pcr_cr_eq]]
               else []
             val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
               [Pretty.block
                     [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
                     Pretty.brk 1,