# HG changeset patch # User wenzelm # Date 1211025270 -7200 # Node ID ca87aff1ad2dbc860c380deaa5b3252522d8804a # Parent 8684b5240f111266d155a43f738e670ad29dde33 structure Display: less pervasive operations; diff -r 8684b5240f11 -r ca87aff1ad2d src/FOLP/classical.ML --- a/src/FOLP/classical.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/FOLP/classical.ML Sat May 17 13:54:30 2008 +0200 @@ -124,10 +124,10 @@ val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = - (writeln"Introduction rules"; prths hazIs; - writeln"Safe introduction rules"; prths safeIs; - writeln"Elimination rules"; prths hazEs; - writeln"Safe elimination rules"; prths safeEs; + (writeln"Introduction rules"; Display.prths hazIs; + writeln"Safe introduction rules"; Display.prths safeIs; + writeln"Elimination rules"; Display.prths hazEs; + writeln"Safe elimination rules"; Display.prths safeEs; ()); fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = diff -r 8684b5240f11 -r ca87aff1ad2d src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/FOLP/simp.ML Sat May 17 13:54:30 2008 +0200 @@ -114,7 +114,7 @@ let fun norm thm = case lhs_of(concl_of thm) of Const(n,_)$_ => n - | _ => (prths normE_thms; error"No constant in lhs of a norm_thm") + | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm") in map norm normE_thms end; fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of @@ -123,7 +123,7 @@ val refl_tac = resolve_tac refl_thms; fun find_res thms thm = - let fun find [] = (prths thms; error"Check Simp_Data") + let fun find [] = (Display.prths thms; error"Check Simp_Data") | find(th::thms) = thm RS th handle THM _ => find thms in find thms end; @@ -250,7 +250,7 @@ fun insert_thm_warn th net = Net.insert_term Thm.eq_thm_prop (concl_of th, th) net handle Net.INSERT => - (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; + (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th; net); val insert_thms = fold_rev insert_thm_warn; @@ -276,7 +276,7 @@ fun delete_thm_warn th net = Net.delete_term Thm.eq_thm_prop (concl_of th, th) net handle Net.DELETE => - (writeln"\nNo such rewrite or congruence rule:"; print_thm th; + (writeln"\nNo such rewrite or congruence rule:"; Display.print_thm th; net); val delete_thms = fold_rev delete_thm_warn; @@ -292,7 +292,7 @@ let fun find((p as (th,ths))::ps',ps) = if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) | find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; - print_thm thm; + Display.print_thm thm; ([],simps')) val (thms,simps') = find(simps,[]) in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, @@ -312,8 +312,8 @@ fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); fun print_ss(SS{congs,simps,...}) = - (writeln"Congruences:"; prths congs; - writeln"Rewrite Rules:"; prths (map #1 simps); ()); + (writeln"Congruences:"; Display.prths congs; + writeln"Rewrite Rules:"; Display.prths (map #1 simps); ()); (* Rewriting with conditionals *) @@ -436,7 +436,7 @@ val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); val anet' = foldr lhs_insert_thm anet rwrls in if !tracing andalso not(null new_rws) - then (writeln"Adding rewrites:"; prths new_rws; ()) + then (writeln"Adding rewrites:"; Display.prths new_rws; ()) else (); (ss,thm,anet',anet::ats,cs) end; diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Import/hol4rews.ML Sat May 17 13:54:30 2008 +0200 @@ -532,7 +532,7 @@ val _ = app (fn (hol,(internal,isa,opt_ty)) => (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); case opt_ty of - SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of thy ty)) ^ "\"") + SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"") | NONE => ())) constmaps val _ = if null constmaps then () diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Import/import_package.ML --- a/src/HOL/Import/import_package.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Import/import_package.ML Sat May 17 13:54:30 2008 +0200 @@ -25,8 +25,8 @@ val debug = ref false fun message s = if !debug then writeln s else () -val string_of_thm = PrintMode.setmp [] string_of_thm; -val string_of_cterm = PrintMode.setmp [] string_of_cterm; +val string_of_thm = PrintMode.setmp [] Display.string_of_thm; +val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm; fun import_tac (thyname,thmname) = if ! quick_and_dirty diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sat May 17 13:54:30 2008 +0200 @@ -205,7 +205,7 @@ Library.setmp show_brackets false ( Library.setmp show_all_types true ( Library.setmp Syntax.ambiguity_is_error false ( - Library.setmp show_sorts true string_of_cterm)))) + Library.setmp show_sorts true Display.string_of_cterm)))) ct) end @@ -227,7 +227,7 @@ | G _ = raise SMART_STRING fun F n = let - val str = Library.setmp show_brackets false (G n string_of_cterm) ct + val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct val u = Syntax.parse_term ctxt str |> TypeInfer.constrain T |> Syntax.check_term ctxt in @@ -236,7 +236,7 @@ else F (n+1) end handle ERROR mesg => F (n+1) - | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct)) + | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct)) in PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 end @@ -244,8 +244,8 @@ val smart_string_of_thm = smart_string_of_cterm o cprop_of -fun prth th = writeln (PrintMode.setmp [] string_of_thm th) -fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct) +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th) +fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ()); fun pth (HOLThm(ren,thm)) = let @@ -1947,14 +1947,14 @@ then let val p1 = quotename constname - val p2 = string_of_ctyp (ctyp_of thy'' ctype) + val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype) val p3 = string_of_mixfix csyn val p4 = smart_string_of_cterm crhs in add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' end else - (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ + (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^ "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) thy'') val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of @@ -2017,7 +2017,7 @@ ((cname,cT,mk_syn thy cname)::cs,p) end) (([],HOLogic.dest_Trueprop (concl_of th)),names) val str = Library.foldl (fn (acc,(c,T,csyn)) => - acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) + acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) val thy' = add_dump str thy val _ = ImportRecorder.add_consts consts in @@ -2143,7 +2143,7 @@ fun add_dump_constdefs thy defname constname rhs ty = let val n = quotename constname - val t = string_of_ctyp (ctyp_of thy ty) + val t = Display.string_of_ctyp (ctyp_of thy ty) val syn = string_of_mixfix (mk_syn thy constname) (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) val eq = quote (constname ^ " == "^rhs) @@ -2228,7 +2228,7 @@ (" apply (rule light_ex_imp_nonempty[where t="^ (proc_prop (cterm_of thy4 t))^"])\n"^ (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 - val str_aty = string_of_ctyp (ctyp_of thy aty) + val str_aty = Display.string_of_ctyp (ctyp_of thy aty) val thy = add_dump_syntax thy rep_name val thy = add_dump_syntax thy abs_name val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Import/shuffler.ML Sat May 17 13:54:30 2008 +0200 @@ -42,7 +42,7 @@ case e of THM (msg,i,thms) => (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); - List.app print_thm thms) + List.app Display.print_thm thms) | THEORY (msg,thys) => (writeln ("Exception THEORY raised:\n" ^ msg); List.app (writeln o Context.str_of_thy) thys) @@ -58,8 +58,8 @@ (*Prints an exception, then fails*) fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e) -val string_of_thm = PrintMode.setmp [] string_of_thm; -val string_of_cterm = PrintMode.setmp [] string_of_cterm; +val string_of_thm = PrintMode.setmp [] Display.string_of_thm; +val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm; fun mk_meta_eq th = (case concl_of th of @@ -305,11 +305,11 @@ in if not (lhs aconv origt) then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; - writeln (string_of_cterm (cterm_of thy origt)); - writeln (string_of_cterm (cterm_of thy lhs)); - writeln (string_of_cterm (cterm_of thy typet)); - writeln (string_of_cterm (cterm_of thy t)); - app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst; + writeln (Display.string_of_cterm (cterm_of thy origt)); + writeln (Display.string_of_cterm (cterm_of thy lhs)); + writeln (Display.string_of_cterm (cterm_of thy typet)); + writeln (Display.string_of_cterm (cterm_of thy t)); + app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; writeln "done") else () end @@ -367,11 +367,11 @@ in if not (lhs aconv origt) then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; - writeln (string_of_cterm (cterm_of thy origt)); - writeln (string_of_cterm (cterm_of thy lhs)); - writeln (string_of_cterm (cterm_of thy typet)); - writeln (string_of_cterm (cterm_of thy t)); - app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst; + writeln (Display.string_of_cterm (cterm_of thy origt)); + writeln (Display.string_of_cterm (cterm_of thy lhs)); + writeln (Display.string_of_cterm (cterm_of thy typet)); + writeln (Display.string_of_cterm (cterm_of thy t)); + app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; writeln "done") else () end diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat May 17 13:54:30 2008 +0200 @@ -159,7 +159,7 @@ fold (fn thm => Data.map (flag thm)) thms_to_be_added context end handle EQVT_FORM s => - error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") + error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") (* in cases of bij- and freshness, we just add the lemmas to the *) (* data-slot *) diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat May 17 13:54:30 2008 +0200 @@ -324,7 +324,7 @@ in (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) handle Option => (writeln "noz: Theorems-Table contains no entry for"; - print_cterm ct ; raise Option))) + Display.print_cterm ct ; raise Option))) end fun unit_conv t = case (term_of t) of @@ -414,7 +414,7 @@ (ds ~~ (map divprop ds)) Inttab.empty in (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) handle Option => (writeln "dvd: Theorems-Table contains no entry for"; - print_cterm ct ; raise Option))) + Display.print_cterm ct ; raise Option))) end val dp = let val th = Simplifier.rewrite lin_ss @@ -485,7 +485,7 @@ sths) Termtab.empty in fn ct => (valOf (Termtab.lookup tab (term_of ct)) - handle Option => (writeln "inS: No theorem for " ; print_cterm ct ; raise Option)) + handle Option => (writeln "inS: No theorem for " ; Display.print_cterm ct ; raise Option)) end val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p in [dp, inf, nb, pd] MRS cpth diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Sat May 17 13:54:30 2008 +0200 @@ -554,10 +554,10 @@ fun say s = if !tracing then writeln s else (); fun print_thms s L = - say (cat_lines (s :: map string_of_thm L)); + say (cat_lines (s :: map Display.string_of_thm L)); fun print_cterms s L = - say (cat_lines (s :: map string_of_cterm L)); + say (cat_lines (s :: map Display.string_of_cterm L)); (*--------------------------------------------------------------------------- @@ -679,7 +679,7 @@ val cntxt = MetaSimplifier.prems_of_ss ss val dummy = print_thms "cntxt:" cntxt val dummy = say "cong rule:" - val dummy = say (string_of_thm thm) + val dummy = say (Display.string_of_thm thm) val dummy = thm_ref := (thm :: !thm_ref) val dummy = ss_ref := (ss :: !ss_ref) (* Unquantified eliminate *) diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Sat May 17 13:54:30 2008 +0200 @@ -298,7 +298,7 @@ raise TFL_ERR "no_repeat_vars" (quote (#1 (dest_Free v)) ^ " occurs repeatedly in the pattern " ^ - quote (string_of_cterm (Thry.typecheck thy pat))) + quote (Display.string_of_cterm (Thry.typecheck thy pat))) else check rst in check (FV_multiset pat) end; @@ -532,7 +532,7 @@ val (extractants,TCl) = ListPair.unzip extracta val dummy = if !trace then (writeln "Extractants = "; - prths extractants; + Display.prths extractants; ()) else () val TCs = foldr (gen_union (op aconv)) [] TCl @@ -553,7 +553,7 @@ |> PureThy.add_defs_i false [Thm.no_attributes (fid ^ "_def", defn)] val def = Thm.freezeT def0; - val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def) + val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def) else () (* val fconst = #lhs(S.dest_eq(concl def)) *) val tych = Thry.typecheck theory @@ -562,7 +562,7 @@ val baz = R.DISCH_ALL (fold_rev R.DISCH full_rqt_prop (R.LIST_CONJ extractants)) - val dum = if !trace then writeln ("baz = " ^ string_of_thm baz) + val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz) else () val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) val SV' = map tych SV; @@ -911,11 +911,11 @@ fun trace_thms s L = - if !trace then writeln (cat_lines (s :: map string_of_thm L)) + if !trace then writeln (cat_lines (s :: map Display.string_of_thm L)) else (); fun trace_cterms s L = - if !trace then writeln (cat_lines (s :: map string_of_cterm L)) + if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L)) else ();; diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Sat May 17 13:54:30 2008 +0200 @@ -40,7 +40,7 @@ fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ - string_of_thm thm); + Display.string_of_thm thm); fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g; diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/inductive_package.ML Sat May 17 13:54:30 2008 +0200 @@ -180,7 +180,7 @@ [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac [le_funI, le_boolI'])) thm))] | _ => [thm] - end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm); + end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm); val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono); val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono); diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat May 17 13:54:30 2008 +0200 @@ -19,7 +19,7 @@ fun name_of_thm thm = (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of [(name, _)] => name - | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm)); + | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/meson.ML Sat May 17 13:54:30 2008 +0200 @@ -121,9 +121,9 @@ let fun forward_tacf [prem] = rtac (nf prem) 1 | forward_tacf prems = error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ - string_of_thm st ^ + Display.string_of_thm st ^ "\nPremises:\n" ^ - cat_lines (map string_of_thm prems)) + cat_lines (map Display.string_of_thm prems)) in case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st) of SOME(th,_) => th @@ -335,7 +335,7 @@ and cnf_nil th = cnf_aux (th,[]) val cls = if too_many_clauses (SOME ctxt) (concl_of th) - then (warning ("cnf is ignoring: " ^ string_of_thm th); ths) + then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths) else cnf_aux (th,ths) in (cls, !ctxtr) end; @@ -535,7 +535,7 @@ | skolemize_nnf_list (th::ths) = skolemize (make_nnf th) :: skolemize_nnf_list ths handle THM _ => (*RS can fail if Unify.search_bound is too small*) - (warning ("Failed to Skolemize " ^ string_of_thm th); + (warning ("Failed to Skolemize " ^ Display.string_of_thm th); skolemize_nnf_list ths); fun add_clauses (th,cls) = @@ -625,9 +625,9 @@ let val horns = make_horns (cls@ths) val _ = Output.debug (fn () => ("meson method called:\n" ^ - space_implode "\n" (map string_of_thm (cls@ths)) ^ + space_implode "\n" (map Display.string_of_thm (cls@ths)) ^ "\nclauses:\n" ^ - space_implode "\n" (map string_of_thm horns))) + space_implode "\n" (map Display.string_of_thm horns))) in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end ); diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/metis_tools.ML Sat May 17 13:54:30 2008 +0200 @@ -270,7 +270,7 @@ fun print_thpair (fth,th) = (Output.debug (fn () => "============================================="); Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth); - Output.debug (fn () => "Isabelle: " ^ string_of_thm th)); + Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th)); fun lookth thpairs (fth : Metis.Thm.thm) = valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) @@ -309,7 +309,7 @@ in SOME (cterm_of thy v, t) end handle Option => (Output.debug (fn() => "List.find failed for the variable " ^ x ^ - " in " ^ string_of_thm i_th); + " in " ^ Display.string_of_thm i_th); NONE) fun remove_typeinst (a, t) = case Recon.strip_prefix ResClause.schematic_var_prefix a of @@ -317,15 +317,15 @@ | NONE => case Recon.strip_prefix ResClause.tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) - val _ = Output.debug (fn () => " isa th: " ^ string_of_thm i_th) + val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm i_th) val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst) val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs) val tms = infer_types ctxt rawtms; val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) val substs' = ListPair.zip (vars, map ctm_of tms) val _ = Output.debug (fn() => "subst_translations:") - val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^ - string_of_cterm y)) + val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^ + Display.string_of_cterm y)) substs' in cterm_instantiate substs' i_th end; @@ -347,8 +347,8 @@ let val thy = ProofContext.theory_of ctxt val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = Output.debug (fn () => " isa th1 (pos): " ^ string_of_thm i_th1) - val _ = Output.debug (fn () => " isa th2 (neg): " ^ string_of_thm i_th2) + val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm i_th1) + val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm i_th2) in if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) else if is_TrueI i_th2 then i_th1 @@ -425,7 +425,7 @@ val _ = Output.debug (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' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst') + val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst') val eq_terms = map (pairself (cterm_of thy)) (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end; @@ -453,7 +453,7 @@ val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf))) - val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th) + val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th) val _ = Output.debug (fn () => "=============================================") val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) in @@ -572,9 +572,9 @@ val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" else (); val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls + val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls val _ = Output.debug (fn () => "THEOREM CLAUSES") - val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths + val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths val {isFO,axioms,tfrees} = build_map mode ctxt cls ths val _ = if null tfrees then () else (Output.debug (fn () => "TFREE CLAUSES"); @@ -597,13 +597,13 @@ val result = translate isFO ctxt' axioms proof and used = List.mapPartial (used_axioms axioms) proof val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => Output.debug (fn () => string_of_thm th)) used + val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs in if null unused then () else warning ("Unused theorems: " ^ commas (map #1 unused)); case result of - (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith) + (_,ith)::_ => (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); ith) | _ => error "METIS: no result" end | Metis.Resolution.Satisfiable _ => error "Metis: No first-order proof with the lemmas supplied" @@ -611,7 +611,7 @@ fun metis_general_tac mode ctxt ths i st0 = let val _ = Output.debug (fn () => - "Metis called with theorems " ^ cat_lines (map string_of_thm ths)) + "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths)) in if exists_type ResAxioms.type_has_empty_sort (prop_of st0) then error "Proof state contains the empty sort" else (); diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Sat May 17 13:54:30 2008 +0200 @@ -32,7 +32,7 @@ val const_of = dest_Const o head_of o fst o dest_eqn; fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ - string_of_thm thm); + Display.string_of_thm thm); fun add_thm opt_module thm = (if Pattern.pattern (lhs_of thm) then diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/res_atp.ML Sat May 17 13:54:30 2008 +0200 @@ -498,10 +498,10 @@ (foldl add_single_names (foldl add_multi_names [] mults) singles) end; -fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false) +fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false) | check_named (_,th) = true; -fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th); +fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th); (* get lemmas from claset, simpset, atpset and extra supplied rules *) fun get_clasimp_atp_lemmas ctxt user_thms = @@ -745,10 +745,10 @@ val _ = Output.debug (fn () => "About to write file " ^ fname) val axcls = make_unique axcls val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)") - val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls + val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls val ccls = subtract_cls ccls axcls val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)") - val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls + val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls val ccltms = map prop_of ccls and axtms = map (prop_of o #1) axcls val subs = tfree_classes_of_terms ccltms @@ -825,7 +825,7 @@ Output.debug (fn () => "subgoals in isar_atp:\n" ^ Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal))); Output.debug (fn () => "current theory: " ^ Context.theory_name thy); - app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths; + app (fn th => Output.debug (fn _ => "chained: " ^ Display.string_of_thm th)) chain_ths; if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal) else (warning ("Writing problem file only: " ^ !problem_name); isar_atp_writeonly (ctxt, chain_ths, goal)) diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/res_axioms.ML Sat May 17 13:54:30 2008 +0200 @@ -176,7 +176,7 @@ (*FIXME: requires more use of cterm constructors*) fun abstract ct = - let val _ = Output.debug (fn()=>" abstraction: " ^ string_of_cterm ct) + let val _ = Output.debug (fn()=>" abstraction: " ^ Display.string_of_cterm ct) val Abs(x,_,body) = term_of ct val thy = theory_of_cterm ct val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) @@ -228,12 +228,12 @@ Abs _ => let val (cv,cta) = Thm.dest_abs NONE ct val (v,Tv) = (dest_Free o term_of) cv - val _ = Output.debug (fn()=>" recursion: " ^ string_of_cterm cta); + val _ = Output.debug (fn()=>" recursion: " ^ Display.string_of_cterm cta); val u_th = combinators_aux cta - val _ = Output.debug (fn()=>" returned " ^ string_of_thm u_th); + val _ = Output.debug (fn()=>" returned " ^ Display.string_of_thm u_th); val cu = Thm.rhs_of u_th val comb_eq = abstract (Thm.cabs cv cu) - in Output.debug (fn()=>" abstraction result: " ^ string_of_thm comb_eq); + in Output.debug (fn()=>" abstraction result: " ^ Display.string_of_thm comb_eq); (transitive (abstract_rule v cv u_th) comb_eq) end | t1 $ t2 => let val (ct1,ct2) = Thm.dest_comb ct @@ -242,13 +242,13 @@ fun combinators th = if lambda_free (prop_of th) then th else - let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th); + let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); val th = Drule.eta_contraction_rule th val eqth = combinators_aux (cprop_of th) - val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth); + val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); in equal_elim eqth th end handle THM (msg,_,_) => - (warning ("Error in the combinator translation of " ^ string_of_thm th); + (warning ("Error in the combinator translation of " ^ Display.string_of_thm th); warning (" Exception message: " ^ msg); TrueI); (*A type variable of sort {} will cause make abstraction fail.*) @@ -311,7 +311,7 @@ fun assert_lambda_free ths msg = case filter (not o lambda_free o prop_of) ths of [] => () - | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths')); + | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths')); (*** Blacklisting (duplicated in ResAtp? ***) @@ -367,7 +367,7 @@ fun name_or_string th = if PureThy.has_name_hint th then PureThy.get_name_hint th - else string_of_thm th; + else Display.string_of_thm th; (*Declare Skolem functions for a theorem, supplied in nnf and with its name. It returns a modified theory, unless skolemization fails.*) @@ -378,7 +378,7 @@ Option.map (fn (nnfth,ctxt1) => let - val _ = Output.debug (fn () => " initial nnf: " ^ string_of_thm nnfth) + val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth) val s = fake_name th val (thy',defs) = declare_skofuns s nnfth thy val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 @@ -531,15 +531,15 @@ (map Thm.term_of hyps) val fixed = term_frees (concl_of st) @ foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps) - in Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st); - Output.debug (fn _ => " st0: " ^ string_of_thm st0); - Output.debug (fn _ => " defs: " ^ commas (map string_of_cterm defs)); + in Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st); + Output.debug (fn _ => " st0: " ^ Display.string_of_thm st0); + Output.debug (fn _ => " defs: " ^ commas (map Display.string_of_cterm defs)); Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; fun meson_general_tac ths i st0 = - let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths)) + let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths)) in (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end; val meson_method_setup = Method.add_methods diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sat May 17 13:54:30 2008 +0200 @@ -38,7 +38,7 @@ fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s else (); -val string_of_thm = PrintMode.setmp [] string_of_thm; +val string_of_thm = PrintMode.setmp [] Display.string_of_thm; (*For generating structured proofs: keep every nth proof line*) val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1; diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Sat May 17 13:54:30 2008 +0200 @@ -164,8 +164,8 @@ fun resolution (c1, hyps1) (c2, hyps2) = let val _ = if !trace_sat then - tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)) - ^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") + tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)) + ^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") else () (* the two literals used for resolution *) @@ -182,7 +182,7 @@ end val _ = if !trace_sat then - tracing ("Resolution theorem: " ^ string_of_thm res_thm) + tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm) else () (* Gamma1, Gamma2 |- False *) @@ -191,7 +191,7 @@ (if hyp1_is_neg then c1' else c2') val _ = if !trace_sat then - tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") + tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") else () val _ = inc counter in @@ -312,7 +312,7 @@ ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause handle TERM ("dest_Trueprop", _) => false) orelse ( - warning ("Ignoring non-clausal premise " ^ string_of_cterm clause); + warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause); false)) clauses' (* remove trivial clauses -- this is necessary because zChaff removes *) (* trivial clauses during preprocessing, and otherwise our clause *) @@ -325,7 +325,7 @@ (* sorted in ascending order *) val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses val _ = if !trace_sat then - tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map string_of_cterm sorted_clauses)) + tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses)) else () (* translate clauses from HOL terms to PropLogic.prop_formula *) val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/specification_package.ML Sat May 17 13:54:30 2008 +0200 @@ -184,7 +184,7 @@ fun add_final (arg as (thy, thm)) = if name = "" then arg |> Library.swap - else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm)); + else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm)); PureThy.store_thm (name, thm) thy) in args |> apsnd (remove_alls frees) diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/watcher.ML --- a/src/HOL/Tools/watcher.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/HOL/Tools/watcher.ML Sat May 17 13:54:30 2008 +0200 @@ -343,10 +343,10 @@ handle OS.SysErr _ => () fun string_of_subgoal th i = - string_of_cterm (List.nth(cprems_of th, i-1)) + Display.string_of_cterm (List.nth(cprems_of th, i-1)) handle Subscript => "Subgoal number out of range!" -fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th)) +fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th)) fun read_proof probfile = let val p = ResReconstruct.txt_path probfile diff -r 8684b5240f11 -r ca87aff1ad2d src/Provers/blast.ML --- a/src/Provers/blast.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Provers/blast.ML Sat May 17 13:54:30 2008 +0200 @@ -495,7 +495,7 @@ end; -fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i; +fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i; (*Resolution/matching tactics: if upd then the proof state may be updated. Matching makes the tactics more deterministic in the presence of Vars.*) @@ -513,11 +513,11 @@ rot_subgoals_tac (rot, #2 trl) i in Option.SOME (trl, tac) end handle ElimBadPrem => (*reject: prems don't preserve conclusion*) - (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl); + (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl); Option.NONE) | ElimBadConcl => (*ignore: conclusion is not just a variable*) (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^ - "conclusion should be a variable\n" ^ string_of_thm rl)) + "conclusion should be a variable\n" ^ Display.string_of_thm rl)) else (); Option.NONE); diff -r 8684b5240f11 -r ca87aff1ad2d src/Provers/classical.ML --- a/src/Provers/classical.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Provers/classical.ML Sat May 17 13:54:30 2008 +0200 @@ -338,13 +338,13 @@ is still allowed.*) fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = if mem_thm safeIs th then - warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) + warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th) else if mem_thm safeEs th then - warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) + warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th) else if mem_thm hazIs th then - warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) + warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th) else if mem_thm hazEs th then - warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) + warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th) else (); @@ -354,7 +354,7 @@ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm safeIs th then - (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); + (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th); cs) else let val th' = flat_rule th @@ -380,10 +380,10 @@ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm safeEs th then - (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); + (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th); cs) else if has_fewer_prems 1 th then - error("Ill-formed elimination rule\n" ^ string_of_thm th) + error("Ill-formed elimination rule\n" ^ Display.string_of_thm th) else let val th' = classical_rule (flat_rule th) @@ -410,7 +410,7 @@ fun make_elim th = if has_fewer_prems 1 th then - error("Ill-formed destruction rule\n" ^ string_of_thm th) + error("Ill-formed destruction rule\n" ^ Display.string_of_thm th) else Tactic.make_elim th; fun cs addSDs ths = cs addSEs (map make_elim ths); @@ -422,7 +422,7 @@ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm hazIs th then - (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); + (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th); cs) else let val th' = flat_rule th @@ -442,16 +442,16 @@ xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair} end handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) - error ("Ill-formed introduction rule\n" ^ string_of_thm th); + error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th); fun addE w th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm hazEs th then - (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); + (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th); cs) else if has_fewer_prems 1 th then - error("Ill-formed elimination rule\n" ^ string_of_thm th) + error("Ill-formed elimination rule\n" ^ Display.string_of_thm th) else let val th' = classical_rule (flat_rule th) @@ -543,7 +543,7 @@ end else cs handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) - error ("Ill-formed introduction rule\n" ^ string_of_thm th); + error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th); fun delE th @@ -572,7 +572,7 @@ mem_thm hazIs th orelse mem_thm hazEs th orelse mem_thm safeEs th' orelse mem_thm hazEs th' then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) - else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs) + else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs) end; fun cs delrules ths = fold delrule ths cs; diff -r 8684b5240f11 -r ca87aff1ad2d src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Pure/Isar/code.ML Sat May 17 13:54:30 2008 +0200 @@ -116,7 +116,7 @@ (** certificate theorems **) fun string_of_lthms r = case Susp.peek r - of SOME thms => (map string_of_thm o rev) thms + of SOME thms => (map Display.string_of_thm o rev) thms | NONE => ["[...]"]; fun pretty_lthms ctxt r = case Susp.peek r @@ -147,7 +147,7 @@ | matches (_ :: _) [] = false | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; fun drop thm' = not (matches args (args_of thm')) - orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false); + orelse (warning ("code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false); val (keeps, drops) = List.partition drop sels; in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end; @@ -537,7 +537,7 @@ let fun cert thm = if const = const_of_func thy thm then thm else error ("Wrong head of defining equation,\nexpected constant " - ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm) + ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm) in map cert thms end; @@ -655,13 +655,13 @@ then thm else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty ^ "\nof defining equation\n" - ^ string_of_thm thm + ^ Display.string_of_thm thm ^ "\nto permitted most general type\n" ^ CodeUnit.string_of_typ thy ty_decl); constrain thm) else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty ^ "\nof defining equation\n" - ^ string_of_thm thm + ^ Display.string_of_thm thm ^ "\nis incompatible with permitted least general type\n" ^ CodeUnit.string_of_typ thy ty_strongest) end; @@ -673,7 +673,7 @@ then thm else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty ^ "\nof defining equation\n" - ^ string_of_thm thm + ^ Display.string_of_thm thm ^ "\nis incompatible with declared function type\n" ^ CodeUnit.string_of_typ thy ty_decl) end; @@ -731,11 +731,11 @@ val c = const_of_func thy func; val _ = if (is_some o AxClass.class_of_param thy) c then error ("Rejected polymorphic equation for overloaded constant:\n" - ^ string_of_thm thm) + ^ Display.string_of_thm thm) else (); val _ = if (is_some o get_datatype_of_constr thy) c then error ("Rejected equation for datatype constructor:\n" - ^ string_of_thm func) + ^ Display.string_of_thm func) else (); in (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default diff -r 8684b5240f11 -r ca87aff1ad2d src/Pure/display.ML --- a/src/Pure/display.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Pure/display.ML Sat May 17 13:54:30 2008 +0200 @@ -11,17 +11,6 @@ val goals_limit: int ref val show_hyps: bool ref val show_tags: bool ref - val string_of_thm: thm -> string - val print_thm: thm -> unit - val print_thms: thm list -> unit - val prth: thm -> thm - val prthq: thm Seq.seq -> thm Seq.seq - val prths: thm list -> thm list - val string_of_ctyp: ctyp -> string - val print_ctyp: ctyp -> unit - val string_of_cterm: cterm -> string - val print_cterm: cterm -> unit - val print_syntax: theory -> unit val show_consts: bool ref end; @@ -31,11 +20,22 @@ val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T val pretty_thm: thm -> Pretty.T + val string_of_thm: thm -> string val pretty_thms: thm list -> Pretty.T val pretty_thm_sg: theory -> thm -> Pretty.T val pretty_thms_sg: theory -> thm list -> Pretty.T + val print_thm: thm -> unit + val print_thms: thm list -> unit + val prth: thm -> thm + val prthq: thm Seq.seq -> thm Seq.seq + val prths: thm list -> thm list val pretty_ctyp: ctyp -> Pretty.T + val string_of_ctyp: ctyp -> string + val print_ctyp: ctyp -> unit val pretty_cterm: cterm -> Pretty.T + val string_of_cterm: cterm -> string + val print_cterm: cterm -> unit + val print_syntax: theory -> unit val pretty_full_theory: bool -> theory -> Pretty.T list val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list val pretty_goals: int -> thm -> Pretty.T list diff -r 8684b5240f11 -r ca87aff1ad2d src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Pure/old_goals.ML Sat May 17 13:54:30 2008 +0200 @@ -201,7 +201,7 @@ case e of THM (msg,i,thms) => (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); - List.app print_thm thms) + List.app Display.print_thm thms) | THEORY (msg,thys) => (writeln ("Exception THEORY raised:\n" ^ msg); List.app (writeln o Context.str_of_thy) thys) diff -r 8684b5240f11 -r ca87aff1ad2d src/Sequents/prover.ML --- a/src/Sequents/prover.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Sequents/prover.ML Sat May 17 13:54:30 2008 +0200 @@ -28,7 +28,7 @@ fun warn_duplicates [] = [] | warn_duplicates dups = - (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups)); + (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups)); dups); fun (Pack(safes,unsafes)) add_safes ths = @@ -51,8 +51,8 @@ fun print_pack (Pack(safes,unsafes)) = - (writeln "Safe rules:"; print_thms safes; - writeln "Unsafe rules:"; print_thms unsafes); + (writeln "Safe rules:"; Display.print_thms safes; + writeln "Unsafe rules:"; Display.print_thms unsafes); (*Returns the list of all formulas in the sequent*) fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u diff -r 8684b5240f11 -r ca87aff1ad2d src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Sequents/simpdata.ML Sat May 17 13:54:30 2008 +0200 @@ -126,7 +126,7 @@ | (Const("Not",_)$_) => th RS iff_reflection_F | _ => th RS iff_reflection_T) | _ => error ("addsimps: unable to use theorem\n" ^ - string_of_thm th)); + Display.string_of_thm th)); (*Replace premises x=y, X<->Y by X==Y*) val mk_meta_prems = diff -r 8684b5240f11 -r ca87aff1ad2d src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/Tools/code/code_funcgr.ML Sat May 17 13:54:30 2008 +0200 @@ -118,7 +118,7 @@ handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.class_error pp e ^ ",\n" ^ "for constant " ^ CodeUnit.string_of_const thy c ^ "\nin defining equations(s)\n" - ^ (cat_lines o map string_of_thm) thms) + ^ (cat_lines o map Display.string_of_thm) thms) (*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*) end; fun match (c, ty) = case tap_typ c @@ -225,7 +225,7 @@ else raise CLASS_ERROR ([c], "Illegal instantation for class operation " ^ CodeUnit.string_of_const thy c ^ "\nin defining equations\n" - ^ (cat_lines o map (string_of_thm o AxClass.overload thy)) thms) + ^ (cat_lines o map (Display.string_of_thm o AxClass.overload thy)) thms) end | NONE => (snd o CodeUnit.head_func) thm; fun add_funcs (const, thms) = @@ -304,7 +304,7 @@ in Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => error ("could not construct evaluation proof (probably due to wellsortedness problem):\n" - ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3]) + ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) end; in proto_eval thy I evaluator end; diff -r 8684b5240f11 -r ca87aff1ad2d src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Fri May 16 23:25:37 2008 +0200 +++ b/src/ZF/Datatype_ZF.thy Sat May 17 13:54:30 2008 +0200 @@ -72,7 +72,7 @@ fun proc sg ss old = let val _ = if !trace then writeln ("data_free: OLD = " ^ - string_of_cterm (cterm_of sg old)) + Display.string_of_cterm (cterm_of sg old)) else () val (lhs,rhs) = FOLogic.dest_eq old val (lhead, largs) = strip_comb lhs @@ -90,7 +90,7 @@ else Const("False",FOLogic.oT) else raise Match val _ = if !trace then - writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) + writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new)) else (); val goal = Logic.mk_equals (old, new) val thm = Goal.prove (Simplifier.the_context ss) [] [] goal diff -r 8684b5240f11 -r ca87aff1ad2d src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri May 16 23:25:37 2008 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sat May 17 13:54:30 2008 +0200 @@ -250,7 +250,7 @@ |> ListPair.map (fn (t, tacs) => Goal.prove_global thy1 [] [] t (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))) - handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg); + handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg); (********) val dummy = writeln " Proving the elimination rule..."; @@ -325,7 +325,7 @@ val dummy = if !Ind_Syntax.trace then (writeln "ind_prems = "; List.app (writeln o Syntax.string_of_term ctxt1) ind_prems; - writeln "raw_induct = "; print_thm raw_induct) + writeln "raw_induct = "; Display.print_thm raw_induct) else (); @@ -356,7 +356,7 @@ ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]); val dummy = if !Ind_Syntax.trace then - (writeln "quant_induct = "; print_thm quant_induct) + (writeln "quant_induct = "; Display.print_thm quant_induct) else (); @@ -431,7 +431,7 @@ else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI}); val dummy = if !Ind_Syntax.trace then - (writeln "lemma = "; print_thm lemma) + (writeln "lemma = "; Display.print_thm lemma) else ();