moved remaining display.ML to more_thm.ML;
authorwenzelm
Fri Sep 25 20:37:59 2015 +0200 (2015-09-25)
changeset 61268abe08fb15a12
parent 61267 0b6217fda81b
child 61269 64a5bce1f498
moved remaining display.ML to more_thm.ML;
NEWS
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/FOLP/classical.ML
src/FOLP/simp.ML
src/HOL/Eisbach/Eisbach_Tools.thy
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Library/Old_SMT/old_smt_solver.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/Library/old_recdef.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/sat.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/element.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/token.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/find_theorems.ML
src/Pure/display.ML
src/Pure/goal_display.ML
src/Pure/more_thm.ML
src/Pure/simplifier.ML
src/Sequents/prover.ML
src/Sequents/simpdata.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_thingol.ML
src/Tools/coherent.ML
src/Tools/induct.ML
src/Tools/nbe.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/NEWS	Fri Sep 25 20:04:25 2015 +0200
     1.2 +++ b/NEWS	Fri Sep 25 20:37:59 2015 +0200
     1.3 @@ -328,6 +328,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* The auxiliary module Pure/display.ML has been eliminated. Its
     1.8 +elementary thm print operations are now in Pure/more_thm.ML and thus
     1.9 +called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
    1.10 +
    1.11  * Simproc programming interfaces have been simplified:
    1.12  Simplifier.make_simproc and Simplifier.define_simproc supersede various
    1.13  forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
     2.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Sep 25 20:04:25 2015 +0200
     2.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Sep 25 20:37:59 2015 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4    fun check_syntax ctxt thm expected =
     2.5      let
     2.6        val obtained =
     2.7 -        Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
     2.8 +        Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm;
     2.9      in
    2.10        if obtained <> expected
    2.11        then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
     3.1 --- a/src/FOLP/classical.ML	Fri Sep 25 20:04:25 2015 +0200
     3.2 +++ b/src/FOLP/classical.ML	Fri Sep 25 20:37:59 2015 +0200
     3.3 @@ -124,10 +124,10 @@
     3.4  
     3.5  fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
     3.6    writeln (cat_lines
     3.7 -   (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
     3.8 -    ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
     3.9 -    ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
    3.10 -    ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
    3.11 +   (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @
    3.12 +    ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @
    3.13 +    ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @
    3.14 +    ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs));
    3.15  
    3.16  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    3.17    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
     4.1 --- a/src/FOLP/simp.ML	Fri Sep 25 20:04:25 2015 +0200
     4.2 +++ b/src/FOLP/simp.ML	Fri Sep 25 20:37:59 2015 +0200
     4.3 @@ -306,8 +306,8 @@
     4.4  
     4.5  fun print_ss ctxt (SS{congs,simps,...}) =
     4.6    writeln (cat_lines
     4.7 -   (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @
     4.8 -    ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps));
     4.9 +   (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @
    4.10 +    ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps));
    4.11  
    4.12  
    4.13  (* Rewriting with conditionals *)
     5.1 --- a/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Sep 25 20:04:25 2015 +0200
     5.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Sep 25 20:37:59 2015 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4        (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
     5.5        (fn ctxt => fn (tok, thms) =>
     5.6          (* FIXME proper formatting!? *)
     5.7 -        Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #>
     5.8 +        Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #>
     5.9      setup_trace_method @{binding print_term}
    5.10        (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
    5.11        (fn ctxt => fn (tok, t) =>
     6.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Fri Sep 25 20:04:25 2015 +0200
     6.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Fri Sep 25 20:37:59 2015 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4  
     6.5  fun drop_fact_warning ctxt =
     6.6    Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
     6.7 -    Display.string_of_thm ctxt)
     6.8 +    Thm.string_of_thm ctxt)
     6.9  
    6.10  
    6.11  (* general theorem normalizations *)
     7.1 --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Fri Sep 25 20:04:25 2015 +0200
     7.2 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Fri Sep 25 20:37:59 2015 +0200
     7.3 @@ -105,7 +105,7 @@
     7.4  
     7.5  fun trace_assms ctxt =
     7.6    Old_SMT_Config.trace_msg ctxt (Pretty.string_of o
     7.7 -    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
     7.8 +    Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
     7.9  
    7.10  fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
    7.11    let
    7.12 @@ -327,7 +327,7 @@
    7.13        if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0
    7.14        then
    7.15          tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
    7.16 -          (map (Display.pretty_thm ctxt o snd) wthms)))
    7.17 +          (map (Thm.pretty_thm ctxt o snd) wthms)))
    7.18        else ()
    7.19      end
    7.20  
     8.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Sep 25 20:04:25 2015 +0200
     8.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Sep 25 20:37:59 2015 +0200
     8.3 @@ -72,7 +72,7 @@
     8.4  fun pretty_goal ctxt thms t =
     8.5    [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
     8.6    |> not (null thms) ? cons (Pretty.big_list "assumptions:"
     8.7 -       (map (Display.pretty_thm ctxt) thms))
     8.8 +       (map (Thm.pretty_thm ctxt) thms))
     8.9  
    8.10  fun try_apply ctxt thms =
    8.11    let
     9.1 --- a/src/HOL/Library/old_recdef.ML	Fri Sep 25 20:04:25 2015 +0200
     9.2 +++ b/src/HOL/Library/old_recdef.ML	Fri Sep 25 20:37:59 2015 +0200
     9.3 @@ -375,8 +375,8 @@
     9.4          (case find_thms_split splitths 1 th of
     9.5            NONE =>
     9.6             (writeln (cat_lines
     9.7 -            (["th:", Display.string_of_thm ctxt th, "split ths:"] @
     9.8 -              map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
     9.9 +            (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
    9.10 +              map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
    9.11              error "splitto: cannot find variable to split on")
    9.12          | SOME v =>
    9.13              let
    9.14 @@ -1342,7 +1342,7 @@
    9.15  fun say s = if !tracing then writeln s else ();
    9.16  
    9.17  fun print_thms ctxt s L =
    9.18 -  say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
    9.19 +  say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
    9.20  
    9.21  fun print_term ctxt s t =
    9.22    say (cat_lines [s, Syntax.string_of_term ctxt t]);
    9.23 @@ -1458,7 +1458,7 @@
    9.24               val cntxt = Simplifier.prems_of ctxt
    9.25               val _ = print_thms ctxt "cntxt:" cntxt
    9.26               val _ = say "cong rule:"
    9.27 -             val _ = say (Display.string_of_thm ctxt thm)
    9.28 +             val _ = say (Thm.string_of_thm ctxt thm)
    9.29               (* Unquantified eliminate *)
    9.30               fun uq_eliminate (thm,imp) =
    9.31                   let val tych = Thm.cterm_of ctxt
    9.32 @@ -2390,7 +2390,7 @@
    9.33  
    9.34  
    9.35  fun trace_thms ctxt s L =
    9.36 -  if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
    9.37 +  if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L))
    9.38    else ();
    9.39  
    9.40  fun trace_cterm ctxt s ct =
    10.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Sep 25 20:04:25 2015 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Sep 25 20:37:59 2015 +0200
    10.3 @@ -156,7 +156,7 @@
    10.4        fold (fn thm => Data.map (flag thm)) thms_to_be_added context
    10.5    end
    10.6    handle EQVT_FORM s =>
    10.7 -      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
    10.8 +      error (Thm.string_of_thm (Context.proof_of context) orig_thm ^ 
    10.9                 " does not comply with the form of an equivariance lemma (" ^ s ^").")
   10.10  
   10.11  
    11.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Sep 25 20:04:25 2015 +0200
    11.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Sep 25 20:37:59 2015 +0200
    11.3 @@ -78,7 +78,7 @@
    11.4       Pretty.chunks (map (fn (b, th) => Pretty.block
    11.5         [Binding.pretty b, Pretty.str ":",
    11.6          Pretty.brk 1,
    11.7 -        Display.pretty_thm ctxt th])
    11.8 +        Thm.pretty_thm ctxt th])
    11.9            defs),
   11.10  
   11.11       Pretty.str "Verification conditions:",
    12.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Sep 25 20:04:25 2015 +0200
    12.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Sep 25 20:37:59 2015 +0200
    12.3 @@ -202,14 +202,14 @@
    12.4            raise QUOT_ERROR [Pretty.block
    12.5              [Pretty.str "The Quotient theorem has extra assumptions:",
    12.6               Pretty.brk 1,
    12.7 -             Display.pretty_thm ctxt quot_thm]]
    12.8 +             Thm.pretty_thm ctxt quot_thm]]
    12.9        else ()
   12.10      val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
   12.11      handle TERM _ => raise QUOT_ERROR
   12.12            [Pretty.block
   12.13              [Pretty.str "The Quotient theorem is not of the right form:",
   12.14               Pretty.brk 1,
   12.15 -             Display.pretty_thm ctxt quot_thm]]
   12.16 +             Thm.pretty_thm ctxt quot_thm]]
   12.17      val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
   12.18      val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
   12.19      val rty_tfreesT = Term.add_tfree_namesT rty []
   12.20 @@ -837,13 +837,13 @@
   12.21                handle TERM _ => raise PCR_ERROR [Pretty.block 
   12.22                      [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
   12.23                      Pretty.brk 1,
   12.24 -                    Display.pretty_thm ctxt pcrel_def]]
   12.25 +                    Thm.pretty_thm ctxt pcrel_def]]
   12.26              val pcr_const_def = head_of def_lhs
   12.27              val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
   12.28                handle TERM _ => raise PCR_ERROR [Pretty.block 
   12.29                      [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
   12.30                      Pretty.brk 1,
   12.31 -                    Display.pretty_thm ctxt pcr_cr_eq]]
   12.32 +                    Thm.pretty_thm ctxt pcr_cr_eq]]
   12.33              val (pcr_const_eq, eqs) = strip_comb eq_lhs
   12.34              fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   12.35                | is_eq _ = false
   12.36 @@ -853,7 +853,7 @@
   12.37                [Pretty.block
   12.38                      [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
   12.39                      Pretty.brk 1,
   12.40 -                    Display.pretty_thm ctxt pcr_cr_eq]]
   12.41 +                    Thm.pretty_thm ctxt pcr_cr_eq]]
   12.42                else []
   12.43              val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
   12.44                [Pretty.block
    13.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Sep 25 20:04:25 2015 +0200
    13.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Sep 25 20:37:59 2015 +0200
    13.3 @@ -186,8 +186,8 @@
    13.4        | tacf prems =
    13.5          error (cat_lines
    13.6            ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    13.7 -            Display.string_of_thm ctxt st ::
    13.8 -            "Premises:" :: map (Display.string_of_thm ctxt) prems))
    13.9 +            Thm.string_of_thm ctxt st ::
   13.10 +            "Premises:" :: map (Thm.string_of_thm ctxt) prems))
   13.11    in
   13.12      case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of
   13.13        SOME (th, _) => th
   13.14 @@ -395,7 +395,7 @@
   13.15        val cls =
   13.16          if has_too_many_clauses ctxt (Thm.concl_of th) then
   13.17            (trace_msg ctxt (fn () =>
   13.18 -               "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   13.19 +               "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths)
   13.20          else
   13.21            cnf_aux (th, ths)
   13.22    in (cls, !ctxt_ref) end
   13.23 @@ -652,7 +652,7 @@
   13.24                                 |> tap (fn NONE =>
   13.25                                            trace_msg ctxt (fn () =>
   13.26                                                "Failed to skolemize " ^
   13.27 -                                               Display.string_of_thm ctxt th)
   13.28 +                                               Thm.string_of_thm ctxt th)
   13.29                                          | _ => ()))
   13.30    end
   13.31  
   13.32 @@ -751,8 +751,8 @@
   13.33            val horns = make_horns (cls @ ths)
   13.34            val _ = trace_msg ctxt (fn () =>
   13.35              cat_lines ("meson method called:" ::
   13.36 -              map (Display.string_of_thm ctxt) (cls @ ths) @
   13.37 -              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   13.38 +              map (Thm.string_of_thm ctxt) (cls @ ths) @
   13.39 +              ["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
   13.40          in
   13.41            THEN_ITER_DEEPEN iter_deepen_limit
   13.42              (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
    14.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Sep 25 20:04:25 2015 +0200
    14.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Sep 25 20:37:59 2015 +0200
    14.3 @@ -170,7 +170,7 @@
    14.4        val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th)
    14.5      in Thm.equal_elim eqth th end
    14.6      handle THM (msg, _, _) =>
    14.7 -           (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^
    14.8 +           (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
    14.9                "\nException message: " ^ msg);
   14.10              (* A type variable of sort "{}" will make "abstraction" fail. *)
   14.11              TrueI)
    15.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Sep 25 20:04:25 2015 +0200
    15.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Sep 25 20:37:59 2015 +0200
    15.3 @@ -134,11 +134,11 @@
    15.4        end
    15.5        handle Option.Option =>
    15.6               (trace_msg ctxt (fn () =>
    15.7 -                "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
    15.8 +                "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
    15.9                NONE)
   15.10             | TYPE _ =>
   15.11               (trace_msg ctxt (fn () =>
   15.12 -                "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
   15.13 +                "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
   15.14                NONE)
   15.15      fun remove_typeinst (a, t) =
   15.16        let val a = Metis_Name.toString a in
   15.17 @@ -149,7 +149,7 @@
   15.18              SOME _ => NONE (* type instantiations are forbidden *)
   15.19            | NONE => SOME (a, t) (* internal Metis var? *)))
   15.20        end
   15.21 -    val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   15.22 +    val _ = trace_msg ctxt (fn () => "  isa th: " ^ Thm.string_of_thm ctxt i_th)
   15.23      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   15.24      val (vars, tms) =
   15.25        ListPair.unzip (map_filter subst_translation substs)
   15.26 @@ -269,8 +269,8 @@
   15.27    let
   15.28      val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2)
   15.29      val _ = trace_msg ctxt (fn () =>
   15.30 -        "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
   15.31 -        \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   15.32 +        "  isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\
   15.33 +        \  isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2)
   15.34    in
   15.35      (* Trivial cases where one operand is type info *)
   15.36      if Thm.eq_thm (TrueI, i_th1) then
   15.37 @@ -369,7 +369,7 @@
   15.38        val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   15.39        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
   15.40        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   15.41 -      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   15.42 +      val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
   15.43        val eq_terms =
   15.44          map (apply2 (Thm.cterm_of ctxt))
   15.45            (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   15.46 @@ -462,7 +462,7 @@
   15.47        val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
   15.48          |> flexflex_first_order ctxt
   15.49          |> resynchronize ctxt fol_th
   15.50 -      val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   15.51 +      val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th)
   15.52        val _ = trace_msg ctxt (fn () => "=============================================")
   15.53      in
   15.54        (fol_th, th) :: th_pairs
    16.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Sep 25 20:04:25 2015 +0200
    16.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Sep 25 20:37:59 2015 +0200
    16.3 @@ -160,7 +160,7 @@
    16.4        val dischargers = map (fst o snd) th_cls_pairs
    16.5        val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
    16.6        val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
    16.7 -      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    16.8 +      val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
    16.9        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   16.10        val type_enc = type_enc_of_string Strict type_enc
   16.11        val (sym_tab, axioms, ord_info, concealed) =
   16.12 @@ -172,7 +172,7 @@
   16.13          | get_isa_thm _ (Isa_Raw ith) = ith
   16.14        val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   16.15        val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
   16.16 -      val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
   16.17 +      val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
   16.18        val _ = trace_msg ctxt (K "METIS CLAUSES")
   16.19        val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
   16.20        val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
   16.21 @@ -200,7 +200,7 @@
   16.22           val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
   16.23           val used = map_filter (used_axioms axioms) proof
   16.24           val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
   16.25 -         val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   16.26 +         val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
   16.27           val (used_th_cls_pairs, unused_th_cls_pairs) =
   16.28             List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
   16.29           val unused_ths = maps (snd o snd) unused_th_cls_pairs
   16.30 @@ -217,7 +217,7 @@
   16.31             ();
   16.32           (case result of
   16.33             (_, ith) :: _ =>
   16.34 -           (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   16.35 +           (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith);
   16.36              [discharge_skolem_premises ctxt dischargers ith])
   16.37           | _ => (trace_msg ctxt (K "Metis: No result"); []))
   16.38         end
   16.39 @@ -251,7 +251,7 @@
   16.40      val unused = Unsynchronized.ref []
   16.41      val type_encs = if null type_encs0 then partial_type_encs else type_encs0
   16.42      val _ = trace_msg ctxt (fn () =>
   16.43 -      "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   16.44 +      "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths))
   16.45      val type_encs = type_encs |> maps unalias_type_enc
   16.46      val combs = (lam_trans = combsN)
   16.47      fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
    17.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Sep 25 20:04:25 2015 +0200
    17.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Sep 25 20:37:59 2015 +0200
    17.3 @@ -355,7 +355,7 @@
    17.4  fun print_intros ctxt gr consts =
    17.5    tracing (cat_lines (map (fn const =>
    17.6      "Constant " ^ const ^ "has intros:\n" ^
    17.7 -    cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
    17.8 +    cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts))
    17.9  
   17.10  
   17.11  (* translation of moded predicates *)
    18.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Sep 25 20:04:25 2015 +0200
    18.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Sep 25 20:37:59 2015 +0200
    18.3 @@ -23,14 +23,14 @@
    18.4      tracing (msg ^
    18.5        (cat_lines (map
    18.6          (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
    18.7 -           commas (map (Display.string_of_thm_global thy) intros)) intross)))
    18.8 +           commas (map (Thm.string_of_thm_global thy) intros)) intross)))
    18.9    else ()
   18.10  
   18.11  fun print_specs options thy specs =
   18.12    if show_intermediate_results options then
   18.13      map (fn (c, thms) =>
   18.14        "Constant " ^ c ^ " has specification:\n" ^
   18.15 -        (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
   18.16 +        (cat_lines (map (Thm.string_of_thm_global thy) thms)) ^ "\n") specs
   18.17      |> cat_lines |> tracing
   18.18    else ()
   18.19  
    19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 25 20:04:25 2015 +0200
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 25 20:37:59 2015 +0200
    19.3 @@ -1079,7 +1079,7 @@
    19.4                  error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
    19.5                    " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
    19.6                    " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
    19.7 -                  " in " ^ Display.string_of_thm ctxt' th)
    19.8 +                  " in " ^ Thm.string_of_thm ctxt' th)
    19.9            in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
   19.10          fun instantiate_typ th =
   19.11            let
    20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 25 20:04:25 2015 +0200
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 25 20:37:59 2015 +0200
    20.3 @@ -130,11 +130,11 @@
    20.4        let
    20.5          val _ = writeln ("predicate: " ^ pred)
    20.6          val _ = writeln ("introrules: ")
    20.7 -        val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
    20.8 +        val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm))
    20.9            (rev (Core_Data.intros_of ctxt pred)) ()
   20.10        in
   20.11          if Core_Data.has_elim ctxt pred then
   20.12 -          writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
   20.13 +          writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
   20.14          else
   20.15            writeln ("no elimrule defined")
   20.16        end
   20.17 @@ -1295,7 +1295,7 @@
   20.18          else
   20.19            error ("Format of introduction rule is invalid: tuples must be expanded:"
   20.20            ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
   20.21 -          (Display.string_of_thm_global thy intro))
   20.22 +          (Thm.string_of_thm_global thy intro))
   20.23        | _ => true
   20.24      val prems = Logic.strip_imp_prems (prop_of intro)
   20.25      fun check_prem (Prem t) = forall check_arg args
   20.26 @@ -1387,7 +1387,7 @@
   20.27      (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
   20.28      val _ =
   20.29        if show_intermediate_results options then
   20.30 -        tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
   20.31 +        tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
   20.32        else ()
   20.33      val (preds, all_vs, param_vs, all_modes, clauses) =
   20.34        prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
    21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Sep 25 20:04:25 2015 +0200
    21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Sep 25 20:37:59 2015 +0200
    21.3 @@ -217,7 +217,7 @@
    21.4      val _ =
    21.5        if show_intermediate_results options then
    21.6          tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
    21.7 -          commas (map (Display.string_of_thm_global thy) spec))
    21.8 +          commas (map (Thm.string_of_thm_global thy) spec))
    21.9        else ()
   21.10    in
   21.11      spec
    22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Sep 25 20:04:25 2015 +0200
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Sep 25 20:37:59 2015 +0200
    22.3 @@ -310,7 +310,7 @@
    22.4  fun rewrite_intro thy intro =
    22.5    let
    22.6      fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
    22.7 -    (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
    22.8 +    (*val _ = tracing ("Rewriting intro " ^ Thm.string_of_thm_global thy intro)*)
    22.9      val intro_t = Logic.unvarify_global (Thm.prop_of intro)
   22.10      val (prems, concl) = Logic.strip_horn intro_t
   22.11      val frees = map fst (Term.add_frees intro_t [])
    23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Sep 25 20:04:25 2015 +0200
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Sep 25 20:37:59 2015 +0200
    23.3 @@ -192,7 +192,7 @@
    23.4  
    23.5  fun print_specs options thy msg ths =
    23.6    if show_intermediate_results options then
    23.7 -    (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
    23.8 +    (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths)))
    23.9    else
   23.10      ()
   23.11  
   23.12 @@ -209,7 +209,7 @@
   23.13            map (rewrite_intros ctxt) specs
   23.14          else
   23.15            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   23.16 -            ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   23.17 +            ^ commas (map (quote o Thm.string_of_thm_global thy) specs))
   23.18        val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
   23.19        val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
   23.20        val _ = print_specs options thy "normalized intros" intros
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 25 20:04:25 2015 +0200
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 25 20:37:59 2015 +0200
    24.3 @@ -306,7 +306,7 @@
    24.4              val (_, ts) = strip_comb t
    24.5            in
    24.6              trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
    24.7 -              " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
    24.8 +              " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm)
    24.9              THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
   24.10                THEN (trace_tac ctxt options "after splitting with split_asm rules")
   24.11              (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
    25.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 25 20:04:25 2015 +0200
    25.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 25 20:37:59 2015 +0200
    25.3 @@ -23,7 +23,7 @@
    25.4  
    25.5  fun drop_fact_warning ctxt =
    25.6    SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
    25.7 -    Display.string_of_thm ctxt)
    25.8 +    Thm.string_of_thm ctxt)
    25.9  
   25.10  
   25.11  (* general theorem normalizations *)
    26.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 25 20:04:25 2015 +0200
    26.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 25 20:37:59 2015 +0200
    26.3 @@ -103,7 +103,7 @@
    26.4  
    26.5  fun trace_assms ctxt =
    26.6    SMT_Config.trace_msg ctxt (Pretty.string_of o
    26.7 -    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
    26.8 +    Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
    26.9  
   26.10  fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) =
   26.11    let
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Sep 25 20:04:25 2015 +0200
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Sep 25 20:37:59 2015 +0200
    27.3 @@ -89,7 +89,7 @@
    27.4      val ctxt = ctxt |> Config.put show_markup true
    27.5      val assms = op @ assmsp
    27.6      val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
    27.7 -    val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
    27.8 +    val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms)
    27.9      val concl = Syntax.pretty_term ctxt concl
   27.10    in
   27.11      tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
    28.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:04:25 2015 +0200
    28.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:37:59 2015 +0200
    28.3 @@ -148,7 +148,7 @@
    28.4              fun add_final (thm, thy) =
    28.5                if name = ""
    28.6                then (thm, thy)
    28.7 -              else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
    28.8 +              else (writeln ("  " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm);
    28.9                  Global_Theory.store_thm (Binding.name name, thm) thy)
   28.10            in
   28.11              swap args
    29.1 --- a/src/HOL/Tools/inductive.ML	Fri Sep 25 20:04:25 2015 +0200
    29.2 +++ b/src/HOL/Tools/inductive.ML	Fri Sep 25 20:37:59 2015 +0200
    29.3 @@ -236,7 +236,7 @@
    29.4          (Pretty.str "(co)inductives:" ::
    29.5            map (Pretty.mark_str o #1)
    29.6              (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
    29.7 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
    29.8 +     Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
    29.9    end |> Pretty.writeln_chunks;
   29.10  
   29.11  
   29.12 @@ -269,7 +269,7 @@
   29.13        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   29.14          (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm))
   29.15      | _ => thm)
   29.16 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
   29.17 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm);
   29.18  
   29.19  val mono_add =
   29.20    Thm.declaration_attribute (fn thm => fn context =>
    30.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Sep 25 20:04:25 2015 +0200
    30.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 25 20:37:59 2015 +0200
    30.3 @@ -298,7 +298,7 @@
    30.4        val _ =
    30.5          if Context_Position.is_really_visible ctxt then
    30.6            warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
    30.7 -            "\n" ^ Display.string_of_thm ctxt thm)
    30.8 +            "\n" ^ Thm.string_of_thm ctxt thm)
    30.9          else ();
   30.10      in tab end;
   30.11  
    31.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Sep 25 20:04:25 2015 +0200
    31.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Sep 25 20:37:59 2015 +0200
    31.3 @@ -303,11 +303,11 @@
    31.4            @{const_name Rings.divide}] a
    31.5      | _ =>
    31.6        (if Context_Position.is_visible ctxt then
    31.7 -        warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
    31.8 +        warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
    31.9         else (); false))
   31.10    | _ =>
   31.11      (if Context_Position.is_visible ctxt then
   31.12 -      warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
   31.13 +      warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
   31.14       else (); false));
   31.15  
   31.16  (* substitute new for occurrences of old in a term, incrementing bound       *)
    32.1 --- a/src/HOL/Tools/sat.ML	Fri Sep 25 20:04:25 2015 +0200
    32.2 +++ b/src/HOL/Tools/sat.ML	Fri Sep 25 20:37:59 2015 +0200
    32.3 @@ -155,9 +155,9 @@
    32.4            let
    32.5              val _ =
    32.6                cond_tracing ctxt (fn () =>
    32.7 -                "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
    32.8 +                "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^
    32.9                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
   32.10 -                ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
   32.11 +                ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^
   32.12                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
   32.13  
   32.14              (* the two literals used for resolution *)
   32.15 @@ -176,7 +176,7 @@
   32.16  
   32.17              val _ =
   32.18                cond_tracing ctxt
   32.19 -                (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
   32.20 +                (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm)
   32.21  
   32.22              (* Gamma1, Gamma2 |- False *)
   32.23              val c_new =
   32.24 @@ -186,7 +186,7 @@
   32.25  
   32.26              val _ =
   32.27                cond_tracing ctxt (fn () =>
   32.28 -                "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
   32.29 +                "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^
   32.30                  " (hyps: " ^
   32.31                  ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
   32.32  
    33.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Sep 25 20:04:25 2015 +0200
    33.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Sep 25 20:37:59 2015 +0200
    33.3 @@ -349,7 +349,7 @@
    33.4  
    33.5  fun trace_thm ctxt msgs th =
    33.6   (if Config.get ctxt LA_Data.trace
    33.7 -  then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th]))
    33.8 +  then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th]))
    33.9    else (); th);
   33.10  
   33.11  fun trace_term ctxt msgs t =
   33.12 @@ -468,8 +468,8 @@
   33.13          if LA_Logic.is_False fls then ()
   33.14          else
   33.15           (tracing (cat_lines
   33.16 -           (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
   33.17 -            ["Proved:", Display.string_of_thm ctxt fls, ""]));
   33.18 +           (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @
   33.19 +            ["Proved:", Thm.string_of_thm ctxt fls, ""]));
   33.20            warning "Linear arithmetic should have refuted the assumptions.\n\
   33.21              \Please inform Tobias Nipkow.")
   33.22      in fls end
    34.1 --- a/src/Provers/blast.ML	Fri Sep 25 20:04:25 2015 +0200
    34.2 +++ b/src/Provers/blast.ML	Fri Sep 25 20:37:59 2015 +0200
    34.3 @@ -484,7 +484,7 @@
    34.4    | cond_tracing false _ = ();
    34.5  
    34.6  fun TRACE ctxt rl tac i st =
    34.7 -  (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st);
    34.8 +  (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st);
    34.9  
   34.10  (*Resolution/matching tactics: if upd then the proof state may be updated.
   34.11    Matching makes the tactics more deterministic in the presence of Vars.*)
   34.12 @@ -509,13 +509,13 @@
   34.13    handle
   34.14      ElimBadPrem => (*reject: prems don't preserve conclusion*)
   34.15        (if Context_Position.is_visible ctxt then
   34.16 -        warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0)
   34.17 +        warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0)
   34.18         else ();
   34.19         Option.NONE)
   34.20    | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   34.21        (cond_tracing (Config.get ctxt trace)
   34.22          (fn () => "Ignoring ill-formed elimination rule:\n" ^
   34.23 -          "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0);
   34.24 +          "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0);
   34.25         Option.NONE);
   34.26  
   34.27  
    35.1 --- a/src/Provers/classical.ML	Fri Sep 25 20:04:25 2015 +0200
    35.2 +++ b/src/Provers/classical.ML	Fri Sep 25 20:37:59 2015 +0200
    35.3 @@ -282,7 +282,7 @@
    35.4  fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
    35.5  fun delete x = delete_tagged_list (joinrules x);
    35.6  
    35.7 -fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th);
    35.8 +fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
    35.9  
   35.10  fun make_elim ctxt th =
   35.11    if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th
   35.12 @@ -290,7 +290,7 @@
   35.13  
   35.14  fun warn_thm ctxt msg th =
   35.15    if Context_Position.is_really_visible ctxt
   35.16 -  then warning (msg ^ Display.string_of_thm ctxt th) else ();
   35.17 +  then warning (msg ^ Thm.string_of_thm ctxt th) else ();
   35.18  
   35.19  fun warn_rules ctxt msg rules (r: rule) =
   35.20    Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true);
   35.21 @@ -634,7 +634,7 @@
   35.22  fun print_claset ctxt =
   35.23    let
   35.24      val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
   35.25 -    val pretty_thms = map (Display.pretty_thm_item ctxt o #1) o Item_Net.content;
   35.26 +    val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content;
   35.27    in
   35.28      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   35.29        Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs),
    36.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 25 20:04:25 2015 +0200
    36.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 25 20:37:59 2015 +0200
    36.3 @@ -532,9 +532,9 @@
    36.4    register_config Proof_Context.show_abbrevs_raw #>
    36.5    register_config Goal_Display.goals_limit_raw #>
    36.6    register_config Goal_Display.show_main_goal_raw #>
    36.7 -  register_config Goal_Display.show_consts_raw #>
    36.8 -  register_config Display.show_hyps_raw #>
    36.9 -  register_config Display.show_tags_raw #>
   36.10 +  register_config Thm.show_consts_raw #>
   36.11 +  register_config Thm.show_hyps_raw #>
   36.12 +  register_config Thm.show_tags_raw #>
   36.13    register_config Pattern.unify_trace_failure_raw #>
   36.14    register_config Unify.trace_bound_raw #>
   36.15    register_config Unify.search_bound_raw #>
    37.1 --- a/src/Pure/Isar/bundle.ML	Fri Sep 25 20:04:25 2015 +0200
    37.2 +++ b/src/Pure/Isar/bundle.ML	Fri Sep 25 20:37:59 2015 +0200
    37.3 @@ -124,7 +124,7 @@
    37.4  
    37.5  fun print_bundles verbose ctxt =
    37.6    let
    37.7 -    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    37.8 +    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
    37.9  
   37.10      fun prt_fact (ths, []) = map prt_thm ths
   37.11        | prt_fact (ths, atts) = Pretty.enclose "(" ")"
    38.1 --- a/src/Pure/Isar/calculation.ML	Fri Sep 25 20:04:25 2015 +0200
    38.2 +++ b/src/Pure/Isar/calculation.ML	Fri Sep 25 20:37:59 2015 +0200
    38.3 @@ -41,7 +41,7 @@
    38.4  
    38.5  fun print_rules ctxt =
    38.6    let
    38.7 -    val pretty_thm = Display.pretty_thm_item ctxt;
    38.8 +    val pretty_thm = Thm.pretty_thm_item ctxt;
    38.9      val (trans, sym) = get_rules ctxt;
   38.10    in
   38.11     [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
   38.12 @@ -137,8 +137,8 @@
   38.13  fun calculate prep_rules final raw_rules int state =
   38.14    let
   38.15      val ctxt = Proof.context_of state;
   38.16 -    val pretty_thm = Display.pretty_thm ctxt;
   38.17 -    val pretty_thm_item = Display.pretty_thm_item ctxt;
   38.18 +    val pretty_thm = Thm.pretty_thm ctxt;
   38.19 +    val pretty_thm_item = Thm.pretty_thm_item ctxt;
   38.20  
   38.21      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   38.22      val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl);
    39.1 --- a/src/Pure/Isar/code.ML	Fri Sep 25 20:04:25 2015 +0200
    39.2 +++ b/src/Pure/Isar/code.ML	Fri Sep 25 20:37:59 2015 +0200
    39.3 @@ -443,11 +443,11 @@
    39.4  exception BAD_THM of string;
    39.5  fun bad_thm msg = raise BAD_THM msg;
    39.6  fun error_thm f thy (thm, proper) = f (thm, proper)
    39.7 -  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
    39.8 +  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
    39.9  fun error_abs_thm f thy thm = f thm
   39.10 -  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
   39.11 +  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
   39.12  fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
   39.13 -  handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE)
   39.14 +  handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE)
   39.15  fun try_thm f thm_proper = SOME (f thm_proper)
   39.16    handle BAD_THM _ => NONE;
   39.17  
   39.18 @@ -764,7 +764,7 @@
   39.19          val (thms, propers) = split_list eqns;
   39.20          val _ = map (fn thm => if c = const_eqn thy thm then ()
   39.21            else error ("Wrong head of code equation,\nexpected constant "
   39.22 -            ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms;
   39.23 +            ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
   39.24          fun tvars_of T = rev (Term.add_tvarsT T []);
   39.25          val vss = map (tvars_of o snd o head_eqn) thms;
   39.26          fun inter_sorts vs =
   39.27 @@ -794,7 +794,7 @@
   39.28      val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
   39.29      val _ = if c = const_abs_eqn thy abs_thm then ()
   39.30        else error ("Wrong head of abstract code equation,\nexpected constant "
   39.31 -        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
   39.32 +        ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm);
   39.33    in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
   39.34  
   39.35  fun constrain_cert_thm thy sorts cert_thm =
   39.36 @@ -888,12 +888,12 @@
   39.37  fun pretty_cert thy (cert as Nothing _) =
   39.38        [Pretty.str "(not implemented)"]
   39.39    | pretty_cert thy (cert as Equations _) =
   39.40 -      (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
   39.41 +      (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
   39.42           o these o snd o equations_of_cert thy) cert
   39.43    | pretty_cert thy (Projection (t, _)) =
   39.44        [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
   39.45    | pretty_cert thy (Abstract (abs_thm, _)) =
   39.46 -      [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
   39.47 +      [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
   39.48  
   39.49  end;
   39.50  
   39.51 @@ -927,7 +927,7 @@
   39.52  fun cert_of_eqns_preprocess ctxt functrans c =
   39.53    let
   39.54      fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
   39.55 -      (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns);
   39.56 +      (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
   39.57      val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
   39.58    in
   39.59      tap (tracing "before function transformation")
   39.60 @@ -1010,7 +1010,7 @@
   39.61      val exec = the_exec thy;
   39.62      fun pretty_equations const thms =
   39.63        (Pretty.block o Pretty.fbreaks)
   39.64 -        (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
   39.65 +        (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
   39.66      fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
   39.67            pretty_equations const (map fst (Lazy.force eqns_lazy))
   39.68        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
   39.69 @@ -1096,7 +1096,7 @@
   39.70          fun drop (thm', proper') = if (proper orelse not proper')
   39.71            andalso matches_args (args_of thm') then 
   39.72              (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
   39.73 -                Display.string_of_thm_global thy thm') else (); true)
   39.74 +                Thm.string_of_thm_global thy thm') else (); true)
   39.75            else false;
   39.76        in (thm, proper) :: filter_out drop eqns end;
   39.77      fun natural_order eqns =
    40.1 --- a/src/Pure/Isar/context_rules.ML	Fri Sep 25 20:04:25 2015 +0200
    40.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Sep 25 20:37:59 2015 +0200
    40.3 @@ -121,7 +121,7 @@
    40.4      fun prt_kind (i, b) =
    40.5        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    40.6          (map_filter (fn (_, (k, th)) =>
    40.7 -            if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
    40.8 +            if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
    40.9            (sort (int_ord o apply2 fst) rules));
   40.10    in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
   40.11  
    41.1 --- a/src/Pure/Isar/element.ML	Fri Sep 25 20:04:25 2015 +0200
    41.2 +++ b/src/Pure/Isar/element.ML	Fri Sep 25 20:37:59 2015 +0200
    41.3 @@ -152,7 +152,7 @@
    41.4    let
    41.5      val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
    41.6      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    41.7 -    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    41.8 +    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
    41.9  
   41.10      fun prt_binding (b, atts) =
   41.11        Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
    42.1 --- a/src/Pure/Isar/local_defs.ML	Fri Sep 25 20:04:25 2015 +0200
    42.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Sep 25 20:37:59 2015 +0200
    42.3 @@ -176,7 +176,7 @@
    42.4  
    42.5  fun print_rules ctxt =
    42.6    Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
    42.7 -    (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
    42.8 +    (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
    42.9  
   42.10  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
   42.11  val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
    43.1 --- a/src/Pure/Isar/method.ML	Fri Sep 25 20:04:25 2015 +0200
    43.2 +++ b/src/Pure/Isar/method.ML	Fri Sep 25 20:37:59 2015 +0200
    43.3 @@ -218,7 +218,7 @@
    43.4  
    43.5  fun trace ctxt rules =
    43.6    if Config.get ctxt rule_trace andalso not (null rules) then
    43.7 -    Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
    43.8 +    Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules)
    43.9      |> Pretty.string_of |> tracing
   43.10    else ();
   43.11  
    44.1 --- a/src/Pure/Isar/obtain.ML	Fri Sep 25 20:04:25 2015 +0200
    44.2 +++ b/src/Pure/Isar/obtain.ML	Fri Sep 25 20:37:59 2015 +0200
    44.3 @@ -257,9 +257,9 @@
    44.4      [prem] =>
    44.5        if Thm.concl_of th aconv thesis andalso
    44.6          Logic.strip_assums_concl prem aconv thesis then th
    44.7 -      else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
    44.8 +      else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th)
    44.9    | [] => error "Goal solved -- nothing guessed"
   44.10 -  | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
   44.11 +  | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th));
   44.12  
   44.13  fun result tac facts ctxt =
   44.14    let
   44.15 @@ -308,7 +308,7 @@
   44.16      val thy = Proof_Context.theory_of ctxt;
   44.17      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
   44.18  
   44.19 -    fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
   44.20 +    fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th);
   44.21  
   44.22      val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
   44.23      val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    45.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 25 20:04:25 2015 +0200
    45.2 +++ b/src/Pure/Isar/proof.ML	Fri Sep 25 20:37:59 2015 +0200
    45.3 @@ -495,7 +495,7 @@
    45.4          error "Bad background theory of goal state";
    45.5      val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
    45.6  
    45.7 -    fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
    45.8 +    fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
    45.9  
   45.10      val th =
   45.11        (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
   45.12 @@ -511,7 +511,7 @@
   45.13        handle THM _ => err_lost ();
   45.14      val _ =
   45.15        Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
   45.16 -        orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
   45.17 +        orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
   45.18  
   45.19      fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
   45.20        | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
    46.1 --- a/src/Pure/Isar/proof_context.ML	Fri Sep 25 20:04:25 2015 +0200
    46.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 25 20:37:59 2015 +0200
    46.3 @@ -396,8 +396,8 @@
    46.4  
    46.5  fun pretty_fact ctxt =
    46.6    let
    46.7 -    val pretty_thm = Display.pretty_thm ctxt;
    46.8 -    val pretty_thms = map (Display.pretty_thm_item ctxt);
    46.9 +    val pretty_thm = Thm.pretty_thm ctxt;
   46.10 +    val pretty_thms = map (Thm.pretty_thm_item ctxt);
   46.11    in
   46.12      fn ("", [th]) => pretty_thm th
   46.13       | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
    47.1 --- a/src/Pure/Isar/proof_display.ML	Fri Sep 25 20:04:25 2015 +0200
    47.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Sep 25 20:37:59 2015 +0200
    47.3 @@ -48,7 +48,7 @@
    47.4    | NONE => Syntax.init_pretty_global (mk_thy ()));
    47.5  
    47.6  fun pp_thm mk_thy th =
    47.7 -  Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
    47.8 +  Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
    47.9  
   47.10  fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
   47.11  fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
   47.12 @@ -215,7 +215,7 @@
   47.13  
   47.14  fun pretty_rule ctxt s thm =
   47.15    Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
   47.16 -    Pretty.fbrk, Display.pretty_thm ctxt thm];
   47.17 +    Pretty.fbrk, Thm.pretty_thm ctxt thm];
   47.18  
   47.19  val string_of_rule = Pretty.string_of ooo pretty_rule;
   47.20  
    48.1 --- a/src/Pure/Isar/runtime.ML	Fri Sep 25 20:04:25 2015 +0200
    48.2 +++ b/src/Pure/Isar/runtime.ML	Fri Sep 25 20:37:59 2015 +0200
    48.3 @@ -119,7 +119,7 @@
    48.4                    (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
    48.5              | THM (msg, i, thms) =>
    48.6                  raised exn ("THM " ^ string_of_int i)
    48.7 -                  (msg :: robust_context context Display.string_of_thm thms)
    48.8 +                  (msg :: robust_context context Thm.string_of_thm thms)
    48.9              | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
   48.10          in [((i, msg), id)] end)
   48.11        and sorted_msgs context exn =
    49.1 --- a/src/Pure/Isar/token.ML	Fri Sep 25 20:04:25 2015 +0200
    49.2 +++ b/src/Pure/Isar/token.ML	Fri Sep 25 20:37:59 2015 +0200
    49.3 @@ -498,7 +498,7 @@
    49.4    | SOME (Typ T) => Syntax.pretty_typ ctxt T
    49.5    | SOME (Term t) => Syntax.pretty_term ctxt t
    49.6    | SOME (Fact (_, ths)) =>
    49.7 -      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
    49.8 +      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
    49.9    | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
   49.10  
   49.11  fun pretty_src ctxt src =
    50.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Sep 25 20:04:25 2015 +0200
    50.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Sep 25 20:37:59 2015 +0200
    50.3 @@ -254,8 +254,8 @@
    50.4        let
    50.5          fun search env [] = error ("Unsolvable constraints:\n" ^
    50.6                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
    50.7 -                Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2
    50.8 -                  (Envir.norm_term bigenv) p)) cs)))
    50.9 +                Thm.pretty_flexpair (Syntax.init_pretty_global thy)
   50.10 +                  (apply2 (Envir.norm_term bigenv) p)) cs)))
   50.11            | search env ((u, p as (t1, t2), vs)::ps) =
   50.12                if u then
   50.13                  let
    51.1 --- a/src/Pure/ROOT	Fri Sep 25 20:04:25 2015 +0200
    51.2 +++ b/src/Pure/ROOT	Fri Sep 25 20:37:59 2015 +0200
    51.3 @@ -247,7 +247,6 @@
    51.4      "context_position.ML"
    51.5      "conv.ML"
    51.6      "defs.ML"
    51.7 -    "display.ML"
    51.8      "drule.ML"
    51.9      "envir.ML"
   51.10      "facts.ML"
    52.1 --- a/src/Pure/ROOT.ML	Fri Sep 25 20:04:25 2015 +0200
    52.2 +++ b/src/Pure/ROOT.ML	Fri Sep 25 20:37:59 2015 +0200
    52.3 @@ -195,7 +195,6 @@
    52.4  use "raw_simplifier.ML";
    52.5  use "conjunction.ML";
    52.6  use "assumption.ML";
    52.7 -use "display.ML";
    52.8  
    52.9  
   52.10  (* Isar -- Intelligible Semi-Automated Reasoning *)
    53.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Sep 25 20:04:25 2015 +0200
    53.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Sep 25 20:37:59 2015 +0200
    53.3 @@ -462,7 +462,7 @@
    53.4  in
    53.5  
    53.6  fun pretty_thm ctxt (thmref, thm) =
    53.7 -  Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
    53.8 +  Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]);
    53.9  
   53.10  fun pretty_theorems state opt_limit rem_dups raw_criteria =
   53.11    let
    54.1 --- a/src/Pure/display.ML	Fri Sep 25 20:04:25 2015 +0200
    54.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    54.3 @@ -1,91 +0,0 @@
    54.4 -(*  Title:      Pure/display.ML
    54.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54.6 -    Author:     Makarius
    54.7 -
    54.8 -Printing of theorems, results etc.
    54.9 -*)
   54.10 -
   54.11 -signature BASIC_DISPLAY =
   54.12 -sig
   54.13 -  val show_consts: bool Config.T
   54.14 -  val show_hyps_raw: Config.raw
   54.15 -  val show_hyps: bool Config.T
   54.16 -  val show_tags_raw: Config.raw
   54.17 -  val show_tags: bool Config.T
   54.18 -end;
   54.19 -
   54.20 -signature DISPLAY =
   54.21 -sig
   54.22 -  include BASIC_DISPLAY
   54.23 -  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
   54.24 -  val pretty_thm: Proof.context -> thm -> Pretty.T
   54.25 -  val pretty_thm_item: Proof.context -> thm -> Pretty.T
   54.26 -  val pretty_thm_global: theory -> thm -> Pretty.T
   54.27 -  val string_of_thm: Proof.context -> thm -> string
   54.28 -  val string_of_thm_global: theory -> thm -> string
   54.29 -end;
   54.30 -
   54.31 -structure Display: DISPLAY =
   54.32 -struct
   54.33 -
   54.34 -(** options **)
   54.35 -
   54.36 -val show_consts = Goal_Display.show_consts;
   54.37 -
   54.38 -val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
   54.39 -val show_hyps = Config.bool show_hyps_raw;
   54.40 -
   54.41 -val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
   54.42 -val show_tags = Config.bool show_tags_raw;
   54.43 -
   54.44 -
   54.45 -
   54.46 -(** print thm **)
   54.47 -
   54.48 -fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
   54.49 -val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
   54.50 -
   54.51 -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   54.52 -  let
   54.53 -    val show_tags = Config.get ctxt show_tags;
   54.54 -    val show_hyps = Config.get ctxt show_hyps;
   54.55 -
   54.56 -    val th = raw_th
   54.57 -      |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
   54.58 -      |> perhaps (try Thm.strip_shyps);
   54.59 -
   54.60 -    val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
   54.61 -    val extra_shyps = Thm.extra_shyps th;
   54.62 -    val tags = Thm.get_tags th;
   54.63 -    val tpairs = Thm.tpairs_of th;
   54.64 -
   54.65 -    val q = if quote then Pretty.quote else I;
   54.66 -    val prt_term = q o Syntax.pretty_term ctxt;
   54.67 -
   54.68 -
   54.69 -    val hlen = length extra_shyps + length hyps + length tpairs;
   54.70 -    val hsymbs =
   54.71 -      if hlen = 0 then []
   54.72 -      else if show_hyps orelse show_hyps' then
   54.73 -        [Pretty.brk 2, Pretty.list "[" "]"
   54.74 -          (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
   54.75 -           map (Syntax.pretty_sort ctxt) extra_shyps)]
   54.76 -      else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
   54.77 -    val tsymbs =
   54.78 -      if null tags orelse not show_tags then []
   54.79 -      else [Pretty.brk 1, pretty_tags tags];
   54.80 -  in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
   54.81 -
   54.82 -fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
   54.83 -fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
   54.84 -
   54.85 -fun pretty_thm_global thy =
   54.86 -  pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
   54.87 -
   54.88 -val string_of_thm = Pretty.string_of oo pretty_thm;
   54.89 -val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
   54.90 -
   54.91 -end;
   54.92 -
   54.93 -structure Basic_Display: BASIC_DISPLAY = Display;
   54.94 -open Basic_Display;
    55.1 --- a/src/Pure/goal_display.ML	Fri Sep 25 20:04:25 2015 +0200
    55.2 +++ b/src/Pure/goal_display.ML	Fri Sep 25 20:37:59 2015 +0200
    55.3 @@ -11,9 +11,6 @@
    55.4    val goals_limit: int Config.T
    55.5    val show_main_goal_raw: Config.raw
    55.6    val show_main_goal: bool Config.T
    55.7 -  val show_consts_raw: Config.raw
    55.8 -  val show_consts: bool Config.T
    55.9 -  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   55.10    val pretty_goals: Proof.context -> thm -> Pretty.T list
   55.11    val pretty_goal: Proof.context -> thm -> Pretty.T
   55.12    val string_of_goal: Proof.context -> thm -> string
   55.13 @@ -28,12 +25,6 @@
   55.14  val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
   55.15  val show_main_goal = Config.bool show_main_goal_raw;
   55.16  
   55.17 -val show_consts_raw = Config.declare_option ("show_consts", @{here});
   55.18 -val show_consts = Config.bool show_consts_raw;
   55.19 -
   55.20 -fun pretty_flexpair ctxt (t, u) = Pretty.block
   55.21 -  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
   55.22 -
   55.23  
   55.24  (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
   55.25  
   55.26 @@ -107,7 +98,7 @@
   55.27        Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
   55.28      val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
   55.29  
   55.30 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
   55.31 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
   55.32  
   55.33      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   55.34      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    56.1 --- a/src/Pure/more_thm.ML	Fri Sep 25 20:04:25 2015 +0200
    56.2 +++ b/src/Pure/more_thm.ML	Fri Sep 25 20:37:59 2015 +0200
    56.3 @@ -9,6 +9,9 @@
    56.4  signature BASIC_THM =
    56.5  sig
    56.6    include BASIC_THM
    56.7 +  val show_consts: bool Config.T
    56.8 +  val show_hyps: bool Config.T
    56.9 +  val show_tags: bool Config.T
   56.10    structure Ctermtab: TABLE
   56.11    structure Thmtab: TABLE
   56.12    val aconvc: cterm * cterm -> bool
   56.13 @@ -105,6 +108,19 @@
   56.14    val kind: string -> attribute
   56.15    val register_proofs: thm list -> theory -> theory
   56.16    val join_theory_proofs: theory -> unit
   56.17 +  val show_consts_raw: Config.raw
   56.18 +  val show_consts: bool Config.T
   56.19 +  val show_hyps_raw: Config.raw
   56.20 +  val show_hyps: bool Config.T
   56.21 +  val show_tags_raw: Config.raw
   56.22 +  val show_tags: bool Config.T
   56.23 +  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   56.24 +  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
   56.25 +  val pretty_thm: Proof.context -> thm -> Pretty.T
   56.26 +  val pretty_thm_item: Proof.context -> thm -> Pretty.T
   56.27 +  val pretty_thm_global: theory -> thm -> Pretty.T
   56.28 +  val string_of_thm: Proof.context -> thm -> string
   56.29 +  val string_of_thm_global: theory -> thm -> string
   56.30  end;
   56.31  
   56.32  structure Thm: THM =
   56.33 @@ -586,6 +602,70 @@
   56.34    Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
   56.35  
   56.36  
   56.37 +
   56.38 +(** print theorems **)
   56.39 +
   56.40 +(* options *)
   56.41 +
   56.42 +val show_consts_raw = Config.declare_option ("show_consts", @{here});
   56.43 +val show_consts = Config.bool show_consts_raw;
   56.44 +
   56.45 +val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
   56.46 +val show_hyps = Config.bool show_hyps_raw;
   56.47 +
   56.48 +val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
   56.49 +val show_tags = Config.bool show_tags_raw;
   56.50 +
   56.51 +
   56.52 +(* pretty_thm etc. *)
   56.53 +
   56.54 +fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
   56.55 +val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
   56.56 +
   56.57 +fun pretty_flexpair ctxt (t, u) = Pretty.block
   56.58 +  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
   56.59 +
   56.60 +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   56.61 +  let
   56.62 +    val show_tags = Config.get ctxt show_tags;
   56.63 +    val show_hyps = Config.get ctxt show_hyps;
   56.64 +
   56.65 +    val th = raw_th
   56.66 +      |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
   56.67 +      |> perhaps (try Thm.strip_shyps);
   56.68 +
   56.69 +    val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
   56.70 +    val extra_shyps = Thm.extra_shyps th;
   56.71 +    val tags = Thm.get_tags th;
   56.72 +    val tpairs = Thm.tpairs_of th;
   56.73 +
   56.74 +    val q = if quote then Pretty.quote else I;
   56.75 +    val prt_term = q o Syntax.pretty_term ctxt;
   56.76 +
   56.77 +
   56.78 +    val hlen = length extra_shyps + length hyps + length tpairs;
   56.79 +    val hsymbs =
   56.80 +      if hlen = 0 then []
   56.81 +      else if show_hyps orelse show_hyps' then
   56.82 +        [Pretty.brk 2, Pretty.list "[" "]"
   56.83 +          (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @
   56.84 +           map (Syntax.pretty_sort ctxt) extra_shyps)]
   56.85 +      else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
   56.86 +    val tsymbs =
   56.87 +      if null tags orelse not show_tags then []
   56.88 +      else [Pretty.brk 1, pretty_tags tags];
   56.89 +  in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
   56.90 +
   56.91 +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
   56.92 +fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
   56.93 +
   56.94 +fun pretty_thm_global thy =
   56.95 +  pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
   56.96 +
   56.97 +val string_of_thm = Pretty.string_of oo pretty_thm;
   56.98 +val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
   56.99 +
  56.100 +
  56.101  open Thm;
  56.102  
  56.103  end;
    57.1 --- a/src/Pure/simplifier.ML	Fri Sep 25 20:04:25 2015 +0200
    57.2 +++ b/src/Pure/simplifier.ML	Fri Sep 25 20:37:59 2015 +0200
    57.3 @@ -162,8 +162,8 @@
    57.4  fun pretty_simpset verbose ctxt =
    57.5    let
    57.6      val pretty_term = Syntax.pretty_term ctxt;
    57.7 -    val pretty_thm = Display.pretty_thm ctxt;
    57.8 -    val pretty_thm_item = Display.pretty_thm_item ctxt;
    57.9 +    val pretty_thm = Thm.pretty_thm ctxt;
   57.10 +    val pretty_thm_item = Thm.pretty_thm_item ctxt;
   57.11  
   57.12      fun pretty_simproc (name, lhss) =
   57.13        Pretty.block
    58.1 --- a/src/Sequents/prover.ML	Fri Sep 25 20:04:25 2015 +0200
    58.2 +++ b/src/Sequents/prover.ML	Fri Sep 25 20:37:59 2015 +0200
    58.3 @@ -63,8 +63,8 @@
    58.4  fun pretty_pack ctxt =
    58.5    let val (safes, unsafes) = get_rules ctxt in
    58.6      Pretty.chunks
    58.7 -     [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes),
    58.8 -      Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)]
    58.9 +     [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes),
   58.10 +      Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)]
   58.11    end;
   58.12  
   58.13  val _ =
   58.14 @@ -82,7 +82,7 @@
   58.15            (case context of
   58.16              Context.Proof ctxt =>
   58.17                if Context_Position.is_really_visible ctxt then
   58.18 -                warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
   58.19 +                warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th)
   58.20                else ()
   58.21            | _ => ());
   58.22        in ths end
    59.1 --- a/src/Sequents/simpdata.ML	Fri Sep 25 20:04:25 2015 +0200
    59.2 +++ b/src/Sequents/simpdata.ML	Fri Sep 25 20:37:59 2015 +0200
    59.3 @@ -38,7 +38,7 @@
    59.4                      | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
    59.5                      | (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
    59.6                      | _                       => th RS @{thm iff_reflection_T})
    59.7 -           | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th));
    59.8 +           | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
    59.9  
   59.10  (*Replace premises x=y, X<->Y by X==Y*)
   59.11  fun mk_meta_prems ctxt =
    60.1 --- a/src/Tools/Code/code_printer.ML	Fri Sep 25 20:04:25 2015 +0200
    60.2 +++ b/src/Tools/Code/code_printer.ML	Fri Sep 25 20:37:59 2015 +0200
    60.3 @@ -111,7 +111,7 @@
    60.4  (** generic nonsense *)
    60.5  
    60.6  fun eqn_error thy (SOME thm) s =
    60.7 -      error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
    60.8 +      error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
    60.9    | eqn_error _ NONE s = error s;
   60.10  
   60.11  val code_presentationN = "code_presentation";
    61.1 --- a/src/Tools/Code/code_thingol.ML	Fri Sep 25 20:04:25 2015 +0200
    61.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Sep 25 20:37:59 2015 +0200
    61.3 @@ -396,7 +396,7 @@
    61.4    else
    61.5      let
    61.6        val thm_msg =
    61.7 -        Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
    61.8 +        Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm;
    61.9        val dep_msg = if null (tl deps) then NONE
   61.10          else SOME ("with dependency "
   61.11            ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
    62.1 --- a/src/Tools/coherent.ML	Fri Sep 25 20:04:25 2015 +0200
    62.2 +++ b/src/Tools/coherent.ML	Fri Sep 25 20:37:59 2015 +0200
    62.3 @@ -175,7 +175,7 @@
    62.4    let
    62.5      val _ =
    62.6        cond_trace ctxt (fn () =>
    62.7 -        Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
    62.8 +        Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
    62.9      val th' =
   62.10        Drule.implies_elim_list
   62.11          (Thm.instantiate
    63.1 --- a/src/Tools/induct.ML	Fri Sep 25 20:04:25 2015 +0200
    63.2 +++ b/src/Tools/induct.ML	Fri Sep 25 20:37:59 2015 +0200
    63.3 @@ -207,7 +207,7 @@
    63.4  
    63.5  fun pretty_rules ctxt kind rs =
    63.6    let val thms = map snd (Item_Net.content rs)
    63.7 -  in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
    63.8 +  in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end;
    63.9  
   63.10  
   63.11  (* context data *)
    64.1 --- a/src/Tools/nbe.ML	Fri Sep 25 20:04:25 2015 +0200
    64.2 +++ b/src/Tools/nbe.ML	Fri Sep 25 20:37:59 2015 +0200
    64.3 @@ -50,17 +50,17 @@
    64.4    let
    64.5      val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
    64.6       of SOME ofclass_eq => ofclass_eq
    64.7 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
    64.8 +      | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm);
    64.9      val (T, class) = case try Logic.dest_of_class ofclass
   64.10       of SOME T_class => T_class
   64.11 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
   64.12 +      | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm);
   64.13      val tvar = case try Term.dest_TVar T
   64.14       of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
   64.15            then tvar
   64.16 -          else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
   64.17 -      | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
   64.18 +          else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm)
   64.19 +      | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm);
   64.20      val _ = if Term.add_tvars eqn [] = [tvar] then ()
   64.21 -      else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
   64.22 +      else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm);
   64.23      val lhs_rhs = case try Logic.dest_equals eqn
   64.24       of SOME lhs_rhs => lhs_rhs
   64.25        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   64.26 @@ -69,7 +69,7 @@
   64.27        | _ => error ("Not an equation with two constants: "
   64.28            ^ Syntax.string_of_term_global thy eqn);
   64.29      val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
   64.30 -      else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
   64.31 +      else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm);
   64.32    in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end;
   64.33  
   64.34  local
    65.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Sep 25 20:04:25 2015 +0200
    65.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Sep 25 20:37:59 2015 +0200
    65.3 @@ -319,7 +319,7 @@
    65.4        if ! Ind_Syntax.trace then
    65.5          writeln (cat_lines
    65.6            (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
    65.7 -           ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
    65.8 +           ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct]))
    65.9        else ();
   65.10  
   65.11  
   65.12 @@ -352,7 +352,7 @@
   65.13  
   65.14       val dummy =
   65.15        if ! Ind_Syntax.trace then
   65.16 -        writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
   65.17 +        writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct)
   65.18        else ();
   65.19  
   65.20  
   65.21 @@ -429,7 +429,7 @@
   65.22  
   65.23       val dummy =
   65.24        if ! Ind_Syntax.trace then
   65.25 -        writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
   65.26 +        writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma)
   65.27        else ();
   65.28  
   65.29  
    66.1 --- a/src/ZF/Tools/typechk.ML	Fri Sep 25 20:04:25 2015 +0200
    66.2 +++ b/src/ZF/Tools/typechk.ML	Fri Sep 25 20:37:59 2015 +0200
    66.3 @@ -26,7 +26,7 @@
    66.4  
    66.5  fun add_rule ctxt th (tcs as TC {rules, net}) =
    66.6    if member Thm.eq_thm_prop rules th then
    66.7 -    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
    66.8 +    (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs)
    66.9    else
   66.10      TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
   66.11  
   66.12 @@ -34,7 +34,7 @@
   66.13    if member Thm.eq_thm_prop rules th then
   66.14      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
   66.15        rules = remove Thm.eq_thm_prop th rules}
   66.16 -  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
   66.17 +  else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs);
   66.18  
   66.19  
   66.20  (* generic data *)
   66.21 @@ -61,7 +61,7 @@
   66.22  fun print_tcset ctxt =
   66.23    let val TC {rules, ...} = tcset_of ctxt in
   66.24      Pretty.writeln (Pretty.big_list "type-checking rules:"
   66.25 -      (map (Display.pretty_thm_item ctxt) rules))
   66.26 +      (map (Thm.pretty_thm_item ctxt) rules))
   66.27    end;
   66.28  
   66.29