# HG changeset patch # User wenzelm # Date 1443206279 -7200 # Node ID abe08fb15a121b4267df9086daf3289c163141e9 # Parent 0b6217fda81b86f7867ac27f161a831570879648 moved remaining display.ML to more_thm.ML; diff -r 0b6217fda81b -r abe08fb15a12 NEWS --- a/NEWS Fri Sep 25 20:04:25 2015 +0200 +++ b/NEWS Fri Sep 25 20:37:59 2015 +0200 @@ -328,6 +328,10 @@ *** ML *** +* The auxiliary module Pure/display.ML has been eliminated. Its +elementary thm print operations are now in Pure/more_thm.ML and thus +called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. + * Simproc programming interfaces have been simplified: Simplifier.make_simproc and Simplifier.define_simproc supersede various forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that diff -r 0b6217fda81b -r abe08fb15a12 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 20:04:25 2015 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 20:37:59 2015 +0200 @@ -151,7 +151,7 @@ fun check_syntax ctxt thm expected = let val obtained = - Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm; + Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm; in if obtained <> expected then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") diff -r 0b6217fda81b -r abe08fb15a12 src/FOLP/classical.ML --- a/src/FOLP/classical.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/FOLP/classical.ML Fri Sep 25 20:37:59 2015 +0200 @@ -124,10 +124,10 @@ fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = writeln (cat_lines - (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @ - ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @ - ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @ - ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs)); + (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @ + ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @ + ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @ + ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs)); fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; diff -r 0b6217fda81b -r abe08fb15a12 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/FOLP/simp.ML Fri Sep 25 20:37:59 2015 +0200 @@ -306,8 +306,8 @@ fun print_ss ctxt (SS{congs,simps,...}) = writeln (cat_lines - (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @ - ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps)); + (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @ + ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps)); (* Rewriting with conditionals *) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Eisbach/Eisbach_Tools.thy --- a/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 20:37:59 2015 +0200 @@ -31,7 +31,7 @@ (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) (fn ctxt => fn (tok, thms) => (* FIXME proper formatting!? *) - Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #> + Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #> setup_trace_method @{binding print_term} (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) (fn ctxt => fn (tok, t) => diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 20:37:59 2015 +0200 @@ -21,7 +21,7 @@ fun drop_fact_warning ctxt = Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Display.string_of_thm ctxt) + Thm.string_of_thm ctxt) (* general theorem normalizations *) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Library/Old_SMT/old_smt_solver.ML --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:37:59 2015 +0200 @@ -105,7 +105,7 @@ fun trace_assms ctxt = Old_SMT_Config.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) + Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) = let @@ -327,7 +327,7 @@ if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0 then tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" - (map (Display.pretty_thm ctxt o snd) wthms))) + (map (Thm.pretty_thm ctxt o snd) wthms))) else () end diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 20:37:59 2015 +0200 @@ -72,7 +72,7 @@ fun pretty_goal ctxt thms t = [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |> not (null thms) ? cons (Pretty.big_list "assumptions:" - (map (Display.pretty_thm ctxt) thms)) + (map (Thm.pretty_thm ctxt) thms)) fun try_apply ctxt thms = let diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Sep 25 20:37:59 2015 +0200 @@ -375,8 +375,8 @@ (case find_thms_split splitths 1 th of NONE => (writeln (cat_lines - (["th:", Display.string_of_thm ctxt th, "split ths:"] @ - map (Display.string_of_thm ctxt) splitths @ ["\n--"])); + (["th:", Thm.string_of_thm ctxt th, "split ths:"] @ + map (Thm.string_of_thm ctxt) splitths @ ["\n--"])); error "splitto: cannot find variable to split on") | SOME v => let @@ -1342,7 +1342,7 @@ fun say s = if !tracing then writeln s else (); fun print_thms ctxt s L = - say (cat_lines (s :: map (Display.string_of_thm ctxt) L)); + say (cat_lines (s :: map (Thm.string_of_thm ctxt) L)); fun print_term ctxt s t = say (cat_lines [s, Syntax.string_of_term ctxt t]); @@ -1458,7 +1458,7 @@ val cntxt = Simplifier.prems_of ctxt val _ = print_thms ctxt "cntxt:" cntxt val _ = say "cong rule:" - val _ = say (Display.string_of_thm ctxt thm) + val _ = say (Thm.string_of_thm ctxt thm) (* Unquantified eliminate *) fun uq_eliminate (thm,imp) = let val tych = Thm.cterm_of ctxt @@ -2390,7 +2390,7 @@ fun trace_thms ctxt s L = - if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L)) + if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L)) else (); fun trace_cterm ctxt s ct = diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 20:37:59 2015 +0200 @@ -156,7 +156,7 @@ fold (fn thm => Data.map (flag thm)) thms_to_be_added context end handle EQVT_FORM s => - error (Display.string_of_thm (Context.proof_of context) orig_thm ^ + error (Thm.string_of_thm (Context.proof_of context) orig_thm ^ " does not comply with the form of an equivariance lemma (" ^ s ^").") diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 20:37:59 2015 +0200 @@ -78,7 +78,7 @@ Pretty.chunks (map (fn (b, th) => Pretty.block [Binding.pretty b, Pretty.str ":", Pretty.brk 1, - Display.pretty_thm ctxt th]) + Thm.pretty_thm ctxt th]) defs), Pretty.str "Verification conditions:", diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 20:37:59 2015 +0200 @@ -202,14 +202,14 @@ 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 [] @@ -837,13 +837,13 @@ 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 @@ -853,7 +853,7 @@ [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 diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 25 20:37:59 2015 +0200 @@ -186,8 +186,8 @@ | tacf prems = error (cat_lines ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: - Display.string_of_thm ctxt st :: - "Premises:" :: map (Display.string_of_thm ctxt) prems)) + Thm.string_of_thm ctxt st :: + "Premises:" :: map (Thm.string_of_thm ctxt) prems)) in case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of SOME (th, _) => th @@ -395,7 +395,7 @@ val cls = if has_too_many_clauses ctxt (Thm.concl_of th) then (trace_msg ctxt (fn () => - "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) + "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths) else cnf_aux (th, ths) in (cls, !ctxt_ref) end @@ -652,7 +652,7 @@ |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^ - Display.string_of_thm ctxt th) + Thm.string_of_thm ctxt th) | _ => ())) end @@ -751,8 +751,8 @@ val horns = make_horns (cls @ ths) val _ = trace_msg ctxt (fn () => cat_lines ("meson method called:" :: - map (Display.string_of_thm ctxt) (cls @ ths) @ - ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) + map (Thm.string_of_thm ctxt) (cls @ ths) @ + ["clauses:"] @ map (Thm.string_of_thm ctxt) horns)) in THEN_ITER_DEEPEN iter_deepen_limit (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 20:37:59 2015 +0200 @@ -170,7 +170,7 @@ val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th) in Thm.equal_elim eqth th end handle THM (msg, _, _) => - (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^ + (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^ "\nException message: " ^ msg); (* A type variable of sort "{}" will make "abstraction" fail. *) TrueI) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 20:37:59 2015 +0200 @@ -134,11 +134,11 @@ end handle Option.Option => (trace_msg ctxt (fn () => - "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) | TYPE _ => (trace_msg ctxt (fn () => - "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = let val a = Metis_Name.toString a in @@ -149,7 +149,7 @@ 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 _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.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) @@ -269,8 +269,8 @@ let val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => - " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\ - \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) + " isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\ + \ isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2) in (* Trivial cases where one operand is type info *) if Thm.eq_thm (TrueI, i_th1) then @@ -369,7 +369,7 @@ val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst') val eq_terms = map (apply2 (Thm.cterm_of ctxt)) (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) @@ -462,7 +462,7 @@ val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) |> flexflex_first_order ctxt |> resynchronize ctxt fol_th - val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th) val _ = trace_msg ctxt (fn () => "=============================================") in (fol_th, th) :: th_pairs diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 20:37:59 2015 +0200 @@ -160,7 +160,7 @@ val dischargers = map (fst o snd) th_cls_pairs val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls + val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_of_string Strict type_enc val (sym_tab, axioms, ord_info, concealed) = @@ -172,7 +172,7 @@ | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (K "ISABELLE CLAUSES") - val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms + val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms val _ = trace_msg ctxt (K "METIS CLAUSES") val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") @@ -200,7 +200,7 @@ val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used + val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used val (used_th_cls_pairs, unused_th_cls_pairs) = List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs val unused_ths = maps (snd o snd) unused_th_cls_pairs @@ -217,7 +217,7 @@ (); (case result of (_, ith) :: _ => - (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) | _ => (trace_msg ctxt (K "Metis: No result"); [])) end @@ -251,7 +251,7 @@ val unused = Unsynchronized.ref [] val type_encs = if null type_encs0 then partial_type_encs else type_encs0 val _ = trace_msg ctxt (fn () => - "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths)) val type_encs = type_encs |> maps unalias_type_enc val combs = (lam_trans = combsN) fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1 diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:37:59 2015 +0200 @@ -355,7 +355,7 @@ fun print_intros ctxt gr consts = tracing (cat_lines (map (fn const => "Constant " ^ const ^ "has intros:\n" ^ - cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts)) + cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts)) (* translation of moded predicates *) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 20:37:59 2015 +0200 @@ -23,14 +23,14 @@ tracing (msg ^ (cat_lines (map (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ - commas (map (Display.string_of_thm_global thy) intros)) intross))) + commas (map (Thm.string_of_thm_global thy) intros)) intross))) else () fun print_specs options thy specs = if show_intermediate_results options then map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ - (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs + (cat_lines (map (Thm.string_of_thm_global thy) thms)) ^ "\n") specs |> cat_lines |> tracing else () diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 20:37:59 2015 +0200 @@ -1079,7 +1079,7 @@ error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^ " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^ " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^ - " in " ^ Display.string_of_thm ctxt' th) + " in " ^ Thm.string_of_thm ctxt' th) in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end fun instantiate_typ th = let diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 20:37:59 2015 +0200 @@ -130,11 +130,11 @@ let val _ = writeln ("predicate: " ^ pred) val _ = writeln ("introrules: ") - val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm)) + val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm)) (rev (Core_Data.intros_of ctxt pred)) () in if Core_Data.has_elim ctxt pred then - writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred)) + writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred)) else writeln ("no elimrule defined") end @@ -1295,7 +1295,7 @@ else error ("Format of introduction rule is invalid: tuples must be expanded:" ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ - (Display.string_of_thm_global thy intro)) + (Thm.string_of_thm_global thy intro)) | _ => true val prems = Logic.strip_imp_prems (prop_of intro) fun check_prem (Prem t) = forall check_arg args @@ -1387,7 +1387,7 @@ (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val _ = if show_intermediate_results options then - tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames))) + tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames))) else () val (preds, all_vs, param_vs, all_modes, clauses) = prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 20:37:59 2015 +0200 @@ -217,7 +217,7 @@ val _ = if show_intermediate_results options then tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^ - commas (map (Display.string_of_thm_global thy) spec)) + commas (map (Thm.string_of_thm_global thy) spec)) else () in spec diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 20:37:59 2015 +0200 @@ -310,7 +310,7 @@ fun rewrite_intro thy intro = let fun lookup_pred t = lookup thy (Fun_Pred.get thy) t - (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*) + (*val _ = tracing ("Rewriting intro " ^ Thm.string_of_thm_global thy intro)*) val intro_t = Logic.unvarify_global (Thm.prop_of intro) val (prems, concl) = Logic.strip_horn intro_t val frees = map fst (Term.add_frees intro_t []) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 20:37:59 2015 +0200 @@ -192,7 +192,7 @@ fun print_specs options thy msg ths = if show_intermediate_results options then - (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) + (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths))) else () @@ -209,7 +209,7 @@ map (rewrite_intros ctxt) specs else error ("unexpected specification for constant " ^ quote constname ^ ":\n" - ^ commas (map (quote o Display.string_of_thm_global thy) specs)) + ^ commas (map (quote o Thm.string_of_thm_global thy) specs)) val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros val _ = print_specs options thy "normalized intros" intros diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 20:37:59 2015 +0200 @@ -306,7 +306,7 @@ val (_, ts) = strip_comb t in trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^ - " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) + " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm) THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1 THEN (trace_tac ctxt options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:37:59 2015 +0200 @@ -23,7 +23,7 @@ fun drop_fact_warning ctxt = SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Display.string_of_thm ctxt) + Thm.string_of_thm ctxt) (* general theorem normalizations *) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 20:37:59 2015 +0200 @@ -103,7 +103,7 @@ fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) + Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) = let diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 20:37:59 2015 +0200 @@ -89,7 +89,7 @@ val ctxt = ctxt |> Config.put show_markup true val assms = op @ assmsp val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") - val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) + val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) val concl = Syntax.pretty_term ctxt concl in tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/choice_specification.ML Fri Sep 25 20:37:59 2015 +0200 @@ -148,7 +148,7 @@ fun add_final (thm, thy) = if name = "" then (thm, thy) - else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); + else (writeln (" " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm); Global_Theory.store_thm (Binding.name name, thm) thy) in swap args diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/inductive.ML Fri Sep 25 20:37:59 2015 +0200 @@ -236,7 +236,7 @@ (Pretty.str "(co)inductives:" :: map (Pretty.mark_str o #1) (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))), - Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] + Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)] end |> Pretty.writeln_chunks; @@ -269,7 +269,7 @@ dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm)) | _ => thm) - end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); + end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm); val mono_add = Thm.declaration_attribute (fn thm => fn context => diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Fri Sep 25 20:37:59 2015 +0200 @@ -298,7 +298,7 @@ val _ = if Context_Position.is_really_visible ctxt then warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^ - "\n" ^ Display.string_of_thm ctxt thm) + "\n" ^ Thm.string_of_thm ctxt thm) else (); in tab end; diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:37:59 2015 +0200 @@ -303,11 +303,11 @@ @{const_name Rings.divide}] a | _ => (if Context_Position.is_visible ctxt then - warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm) + warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)) | _ => (if Context_Position.is_visible ctxt then - warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm) + warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)); (* substitute new for occurrences of old in a term, incrementing bound *) diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/sat.ML Fri Sep 25 20:37:59 2015 +0200 @@ -155,9 +155,9 @@ let val _ = cond_tracing ctxt (fn () => - "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^ + "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^ - ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^ + ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")") (* the two literals used for resolution *) @@ -176,7 +176,7 @@ val _ = cond_tracing ctxt - (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm) + (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm) (* Gamma1, Gamma2 |- False *) val c_new = @@ -186,7 +186,7 @@ val _ = cond_tracing ctxt (fn () => - "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^ + "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")") diff -r 0b6217fda81b -r abe08fb15a12 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 20:37:59 2015 +0200 @@ -349,7 +349,7 @@ fun trace_thm ctxt msgs th = (if Config.get ctxt LA_Data.trace - then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th])) + then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th])) else (); th); fun trace_term ctxt msgs t = @@ -468,8 +468,8 @@ if LA_Logic.is_False fls then () else (tracing (cat_lines - (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @ - ["Proved:", Display.string_of_thm ctxt fls, ""])); + (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @ + ["Proved:", Thm.string_of_thm ctxt fls, ""])); warning "Linear arithmetic should have refuted the assumptions.\n\ \Please inform Tobias Nipkow.") in fls end diff -r 0b6217fda81b -r abe08fb15a12 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Provers/blast.ML Fri Sep 25 20:37:59 2015 +0200 @@ -484,7 +484,7 @@ | cond_tracing false _ = (); fun TRACE ctxt rl tac i st = - (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st); + (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st); (*Resolution/matching tactics: if upd then the proof state may be updated. Matching makes the tactics more deterministic in the presence of Vars.*) @@ -509,13 +509,13 @@ handle ElimBadPrem => (*reject: prems don't preserve conclusion*) (if Context_Position.is_visible ctxt then - warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0) + warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0) else (); Option.NONE) | ElimBadConcl => (*ignore: conclusion is not just a variable*) (cond_tracing (Config.get ctxt trace) (fn () => "Ignoring ill-formed elimination rule:\n" ^ - "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0); + "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0); Option.NONE); diff -r 0b6217fda81b -r abe08fb15a12 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Provers/classical.ML Fri Sep 25 20:37:59 2015 +0200 @@ -282,7 +282,7 @@ fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; fun delete x = delete_tagged_list (joinrules x); -fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th); +fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); fun make_elim ctxt th = if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th @@ -290,7 +290,7 @@ fun warn_thm ctxt msg th = if Context_Position.is_really_visible ctxt - then warning (msg ^ Display.string_of_thm ctxt th) else (); + then warning (msg ^ Thm.string_of_thm ctxt th) else (); fun warn_rules ctxt msg rules (r: rule) = Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true); @@ -634,7 +634,7 @@ fun print_claset ctxt = let val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; - val pretty_thms = map (Display.pretty_thm_item ctxt o #1) o Item_Net.content; + val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content; in [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Sep 25 20:37:59 2015 +0200 @@ -532,9 +532,9 @@ register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> - register_config Goal_Display.show_consts_raw #> - register_config Display.show_hyps_raw #> - register_config Display.show_tags_raw #> + register_config Thm.show_consts_raw #> + register_config Thm.show_hyps_raw #> + register_config Thm.show_tags_raw #> register_config Pattern.unify_trace_failure_raw #> register_config Unify.trace_bound_raw #> register_config Unify.search_bound_raw #> diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/bundle.ML Fri Sep 25 20:37:59 2015 +0200 @@ -124,7 +124,7 @@ fun print_bundles verbose ctxt = let - val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; + val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; fun prt_fact (ths, []) = map prt_thm ths | prt_fact (ths, atts) = Pretty.enclose "(" ")" diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/calculation.ML Fri Sep 25 20:37:59 2015 +0200 @@ -41,7 +41,7 @@ fun print_rules ctxt = let - val pretty_thm = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm_item ctxt; val (trans, sym) = get_rules ctxt; in [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)), @@ -137,8 +137,8 @@ fun calculate prep_rules final raw_rules int state = let val ctxt = Proof.context_of state; - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thm_item = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thm_item = Thm.pretty_thm_item ctxt; val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl); diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/code.ML Fri Sep 25 20:37:59 2015 +0200 @@ -443,11 +443,11 @@ exception BAD_THM of string; fun bad_thm msg = raise BAD_THM msg; fun error_thm f thy (thm, proper) = f (thm, proper) - handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); + handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); fun error_abs_thm f thy thm = f thm - handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); + handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); fun warning_thm f thy (thm, proper) = SOME (f (thm, proper)) - handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE) + handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE) fun try_thm f thm_proper = SOME (f thm_proper) handle BAD_THM _ => NONE; @@ -764,7 +764,7 @@ val (thms, propers) = split_list eqns; val _ = map (fn thm => if c = const_eqn thy thm then () else error ("Wrong head of code equation,\nexpected constant " - ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms; + ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms; fun tvars_of T = rev (Term.add_tvarsT T []); val vss = map (tvars_of o snd o head_eqn) thms; fun inter_sorts vs = @@ -794,7 +794,7 @@ val _ = assert_abs_eqn thy (SOME tyco) abs_thm; val _ = if c = const_abs_eqn thy abs_thm then () else error ("Wrong head of abstract code equation,\nexpected constant " - ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm); + ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm); in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; fun constrain_cert_thm thy sorts cert_thm = @@ -888,12 +888,12 @@ fun pretty_cert thy (cert as Nothing _) = [Pretty.str "(not implemented)"] | pretty_cert thy (cert as Equations _) = - (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd) + (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd) o these o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = [Syntax.pretty_term_global thy (Logic.varify_types_global t)] | pretty_cert thy (Abstract (abs_thm, _)) = - [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; + [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; end; @@ -927,7 +927,7 @@ fun cert_of_eqns_preprocess ctxt functrans c = let fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) - (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns); + (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns); val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) (); in tap (tracing "before function transformation") @@ -1010,7 +1010,7 @@ val exec = the_exec thy; fun pretty_equations const thms = (Pretty.block o Pretty.fbreaks) - (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms); + (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); fun pretty_function (const, Eqns_Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy)) | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) @@ -1096,7 +1096,7 @@ fun drop (thm', proper') = if (proper orelse not proper') andalso matches_args (args_of thm') then (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ - Display.string_of_thm_global thy thm') else (); true) + Thm.string_of_thm_global thy thm') else (); true) else false; in (thm, proper) :: filter_out drop eqns end; fun natural_order eqns = diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/context_rules.ML Fri Sep 25 20:37:59 2015 +0200 @@ -121,7 +121,7 @@ fun prt_kind (i, b) = Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") (map_filter (fn (_, (k, th)) => - if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) + if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE) (sort (int_ord o apply2 fst) rules)); in Pretty.writeln_chunks (map prt_kind rule_kinds) end; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/element.ML Fri Sep 25 20:37:59 2015 +0200 @@ -152,7 +152,7 @@ let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; - val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; + val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; fun prt_binding (b, atts) = Attrib.pretty_binding ctxt (b, if show_attribs then atts else []); diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/local_defs.ML Fri Sep 25 20:37:59 2015 +0200 @@ -176,7 +176,7 @@ fun print_rules ctxt = Pretty.writeln (Pretty.big_list "definitional rewrite rules:" - (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); + (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context); val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context); diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/method.ML Fri Sep 25 20:37:59 2015 +0200 @@ -218,7 +218,7 @@ fun trace ctxt rules = if Config.get ctxt rule_trace andalso not (null rules) then - Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) + Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) |> Pretty.string_of |> tracing else (); diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Sep 25 20:37:59 2015 +0200 @@ -257,9 +257,9 @@ [prem] => if Thm.concl_of th aconv thesis andalso Logic.strip_assums_concl prem aconv thesis then th - else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th) + else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th) | [] => error "Goal solved -- nothing guessed" - | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th)); + | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th)); fun result tac facts ctxt = let @@ -308,7 +308,7 @@ val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); - fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); + fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; val rule = Thm.incr_indexes (maxidx + 1) raw_rule; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/proof.ML Fri Sep 25 20:37:59 2015 +0200 @@ -495,7 +495,7 @@ error "Bad background theory of goal state"; val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); - fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); + fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal); val th = (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) @@ -511,7 +511,7 @@ handle THM _ => err_lost (); val _ = Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results)) - orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th); + orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th); fun recover_result ([] :: pss) thss = [] :: recover_result pss thss | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Sep 25 20:37:59 2015 +0200 @@ -396,8 +396,8 @@ fun pretty_fact ctxt = let - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thms = map (Display.pretty_thm_item ctxt); + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/proof_display.ML Fri Sep 25 20:37:59 2015 +0200 @@ -48,7 +48,7 @@ | NONE => Syntax.init_pretty_global (mk_thy ())); fun pp_thm mk_thy th = - Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; + Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T); fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t); @@ -215,7 +215,7 @@ fun pretty_rule ctxt s thm = Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), - Pretty.fbrk, Display.pretty_thm ctxt thm]; + Pretty.fbrk, Thm.pretty_thm ctxt thm]; val string_of_rule = Pretty.string_of ooo pretty_rule; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/runtime.ML Fri Sep 25 20:37:59 2015 +0200 @@ -119,7 +119,7 @@ (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts)) | THM (msg, i, thms) => raised exn ("THM " ^ string_of_int i) - (msg :: robust_context context Display.string_of_thm thms) + (msg :: robust_context context Thm.string_of_thm thms) | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); in [((i, msg), id)] end) and sorted_msgs context exn = diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Isar/token.ML Fri Sep 25 20:37:59 2015 +0200 @@ -498,7 +498,7 @@ | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => - Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths)) + Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); fun pretty_src ctxt src = diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Proof/reconstruct.ML Fri Sep 25 20:37:59 2015 +0200 @@ -254,8 +254,8 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2 - (Envir.norm_term bigenv) p)) cs))) + Thm.pretty_flexpair (Syntax.init_pretty_global thy) + (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then let diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/ROOT --- a/src/Pure/ROOT Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/ROOT Fri Sep 25 20:37:59 2015 +0200 @@ -247,7 +247,6 @@ "context_position.ML" "conv.ML" "defs.ML" - "display.ML" "drule.ML" "envir.ML" "facts.ML" diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/ROOT.ML Fri Sep 25 20:37:59 2015 +0200 @@ -195,7 +195,6 @@ use "raw_simplifier.ML"; use "conjunction.ML"; use "assumption.ML"; -use "display.ML"; (* Isar -- Intelligible Semi-Automated Reasoning *) diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Sep 25 20:37:59 2015 +0200 @@ -462,7 +462,7 @@ in fun pretty_thm ctxt (thmref, thm) = - Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]); + Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]); fun pretty_theorems state opt_limit rem_dups raw_criteria = let diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/display.ML --- a/src/Pure/display.ML Fri Sep 25 20:04:25 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,91 +0,0 @@ -(* Title: Pure/display.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Makarius - -Printing of theorems, results etc. -*) - -signature BASIC_DISPLAY = -sig - val show_consts: bool Config.T - val show_hyps_raw: Config.raw - val show_hyps: bool Config.T - val show_tags_raw: Config.raw - val show_tags: bool Config.T -end; - -signature DISPLAY = -sig - include BASIC_DISPLAY - val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T - val pretty_thm: Proof.context -> thm -> Pretty.T - val pretty_thm_item: Proof.context -> thm -> Pretty.T - val pretty_thm_global: theory -> thm -> Pretty.T - val string_of_thm: Proof.context -> thm -> string - val string_of_thm_global: theory -> thm -> string -end; - -structure Display: DISPLAY = -struct - -(** options **) - -val show_consts = Goal_Display.show_consts; - -val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false); -val show_hyps = Config.bool show_hyps_raw; - -val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false); -val show_tags = Config.bool show_tags_raw; - - - -(** print thm **) - -fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; -val pretty_tags = Pretty.list "[" "]" o map pretty_tag; - -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = - let - val show_tags = Config.get ctxt show_tags; - val show_hyps = Config.get ctxt show_hyps; - - val th = raw_th - |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt))) - |> perhaps (try Thm.strip_shyps); - - val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th; - val extra_shyps = Thm.extra_shyps th; - val tags = Thm.get_tags th; - val tpairs = Thm.tpairs_of th; - - val q = if quote then Pretty.quote else I; - val prt_term = q o Syntax.pretty_term ctxt; - - - val hlen = length extra_shyps + length hyps + length tpairs; - val hsymbs = - if hlen = 0 then [] - else if show_hyps orelse show_hyps' then - [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ - map (Syntax.pretty_sort ctxt) extra_shyps)] - else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; - val tsymbs = - if null tags orelse not show_tags then [] - else [Pretty.brk 1, pretty_tags tags]; - in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; - -fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; -fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; - -fun pretty_thm_global thy = - pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; - -val string_of_thm = Pretty.string_of oo pretty_thm; -val string_of_thm_global = Pretty.string_of oo pretty_thm_global; - -end; - -structure Basic_Display: BASIC_DISPLAY = Display; -open Basic_Display; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/goal_display.ML Fri Sep 25 20:37:59 2015 +0200 @@ -11,9 +11,6 @@ val goals_limit: int Config.T val show_main_goal_raw: Config.raw val show_main_goal: bool Config.T - val show_consts_raw: Config.raw - val show_consts: bool Config.T - val pretty_flexpair: Proof.context -> term * term -> Pretty.T val pretty_goals: Proof.context -> thm -> Pretty.T list val pretty_goal: Proof.context -> thm -> Pretty.T val string_of_goal: Proof.context -> thm -> string @@ -28,12 +25,6 @@ val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here}); val show_main_goal = Config.bool show_main_goal_raw; -val show_consts_raw = Config.declare_option ("show_consts", @{here}); -val show_consts = Config.bool show_consts_raw; - -fun pretty_flexpair ctxt (t, u) = Pretty.block - [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; - (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) @@ -107,7 +98,7 @@ Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A]; val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A); - val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt); + val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt); val pretty_consts = pretty_list "constants:" prt_consts o consts_of; val pretty_vars = pretty_list "variables:" prt_vars o vars_of; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/more_thm.ML Fri Sep 25 20:37:59 2015 +0200 @@ -9,6 +9,9 @@ signature BASIC_THM = sig include BASIC_THM + val show_consts: bool Config.T + val show_hyps: bool Config.T + val show_tags: bool Config.T structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool @@ -105,6 +108,19 @@ val kind: string -> attribute val register_proofs: thm list -> theory -> theory val join_theory_proofs: theory -> unit + val show_consts_raw: Config.raw + val show_consts: bool Config.T + val show_hyps_raw: Config.raw + val show_hyps: bool Config.T + val show_tags_raw: Config.raw + val show_tags: bool Config.T + val pretty_flexpair: Proof.context -> term * term -> Pretty.T + val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T + val pretty_thm: Proof.context -> thm -> Pretty.T + val pretty_thm_item: Proof.context -> thm -> Pretty.T + val pretty_thm_global: theory -> thm -> Pretty.T + val string_of_thm: Proof.context -> thm -> string + val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = @@ -586,6 +602,70 @@ Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy))); + +(** print theorems **) + +(* options *) + +val show_consts_raw = Config.declare_option ("show_consts", @{here}); +val show_consts = Config.bool show_consts_raw; + +val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false); +val show_hyps = Config.bool show_hyps_raw; + +val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false); +val show_tags = Config.bool show_tags_raw; + + +(* pretty_thm etc. *) + +fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; +val pretty_tags = Pretty.list "[" "]" o map pretty_tag; + +fun pretty_flexpair ctxt (t, u) = Pretty.block + [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; + +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = + let + val show_tags = Config.get ctxt show_tags; + val show_hyps = Config.get ctxt show_hyps; + + val th = raw_th + |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt))) + |> perhaps (try Thm.strip_shyps); + + val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; + val extra_shyps = Thm.extra_shyps th; + val tags = Thm.get_tags th; + val tpairs = Thm.tpairs_of th; + + val q = if quote then Pretty.quote else I; + val prt_term = q o Syntax.pretty_term ctxt; + + + val hlen = length extra_shyps + length hyps + length tpairs; + val hsymbs = + if hlen = 0 then [] + else if show_hyps orelse show_hyps' then + [Pretty.brk 2, Pretty.list "[" "]" + (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @ + map (Syntax.pretty_sort ctxt) extra_shyps)] + else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; + val tsymbs = + if null tags orelse not show_tags then [] + else [Pretty.brk 1, pretty_tags tags]; + in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; + +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; +fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; + +fun pretty_thm_global thy = + pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; + +val string_of_thm = Pretty.string_of oo pretty_thm; +val string_of_thm_global = Pretty.string_of oo pretty_thm_global; + + open Thm; end; diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Pure/simplifier.ML Fri Sep 25 20:37:59 2015 +0200 @@ -162,8 +162,8 @@ fun pretty_simpset verbose ctxt = let val pretty_term = Syntax.pretty_term ctxt; - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thm_item = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thm_item = Thm.pretty_thm_item ctxt; fun pretty_simproc (name, lhss) = Pretty.block diff -r 0b6217fda81b -r abe08fb15a12 src/Sequents/prover.ML --- a/src/Sequents/prover.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Sequents/prover.ML Fri Sep 25 20:37:59 2015 +0200 @@ -63,8 +63,8 @@ fun pretty_pack ctxt = let val (safes, unsafes) = get_rules ctxt in Pretty.chunks - [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes), - Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)] + [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes), + Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)] end; val _ = @@ -82,7 +82,7 @@ (case context of Context.Proof ctxt => if Context_Position.is_really_visible ctxt then - warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th) + warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th) else () | _ => ()); in ths end diff -r 0b6217fda81b -r abe08fb15a12 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Sequents/simpdata.ML Fri Sep 25 20:37:59 2015 +0200 @@ -38,7 +38,7 @@ | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} | (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} | _ => th RS @{thm iff_reflection_T}) - | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th)); + | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); (*Replace premises x=y, X<->Y by X==Y*) fun mk_meta_prems ctxt = diff -r 0b6217fda81b -r abe08fb15a12 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/Code/code_printer.ML Fri Sep 25 20:37:59 2015 +0200 @@ -111,7 +111,7 @@ (** generic nonsense *) fun eqn_error thy (SOME thm) s = - error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm) + error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm) | eqn_error _ NONE s = error s; val code_presentationN = "code_presentation"; diff -r 0b6217fda81b -r abe08fb15a12 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Sep 25 20:37:59 2015 +0200 @@ -396,7 +396,7 @@ else let val thm_msg = - Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm; + Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm; val dep_msg = if null (tl deps) then NONE else SOME ("with dependency " ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); diff -r 0b6217fda81b -r abe08fb15a12 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/coherent.ML Fri Sep 25 20:37:59 2015 +0200 @@ -175,7 +175,7 @@ let val _ = cond_trace ctxt (fn () => - Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms))); + Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms))); val th' = Drule.implies_elim_list (Thm.instantiate diff -r 0b6217fda81b -r abe08fb15a12 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/induct.ML Fri Sep 25 20:37:59 2015 +0200 @@ -207,7 +207,7 @@ fun pretty_rules ctxt kind rs = let val thms = map snd (Item_Net.content rs) - in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end; + in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end; (* context data *) diff -r 0b6217fda81b -r abe08fb15a12 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/nbe.ML Fri Sep 25 20:37:59 2015 +0200 @@ -50,17 +50,17 @@ let val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) of SOME ofclass_eq => ofclass_eq - | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm); + | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val (T, class) = case try Logic.dest_of_class ofclass of SOME T_class => T_class - | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm); + | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val tvar = case try Term.dest_TVar T of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort) then tvar - else error ("Bad sort: " ^ Display.string_of_thm_global thy thm) - | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm); + else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm) + | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm); val _ = if Term.add_tvars eqn [] = [tvar] then () - else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm); + else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm); val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); @@ -69,7 +69,7 @@ | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then () - else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm); + else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm); in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end; local diff -r 0b6217fda81b -r abe08fb15a12 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Sep 25 20:37:59 2015 +0200 @@ -319,7 +319,7 @@ if ! Ind_Syntax.trace then writeln (cat_lines (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @ - ["raw_induct:", Display.string_of_thm ctxt1 raw_induct])) + ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct])) else (); @@ -352,7 +352,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct) + writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct) else (); @@ -429,7 +429,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma) + writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma) else (); diff -r 0b6217fda81b -r abe08fb15a12 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/ZF/Tools/typechk.ML Fri Sep 25 20:37:59 2015 +0200 @@ -26,7 +26,7 @@ fun add_rule ctxt th (tcs as TC {rules, net}) = if member Thm.eq_thm_prop rules th then - (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs) + (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs) else TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net}; @@ -34,7 +34,7 @@ if member Thm.eq_thm_prop rules th then TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, rules = remove Thm.eq_thm_prop th rules} - else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs); + else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs); (* generic data *) @@ -61,7 +61,7 @@ fun print_tcset ctxt = let val TC {rules, ...} = tcset_of ctxt in Pretty.writeln (Pretty.big_list "type-checking rules:" - (map (Display.pretty_thm_item ctxt) rules)) + (map (Thm.pretty_thm_item ctxt) rules)) end;