--- 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 =
--- 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;
--- 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 ()
--- 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
--- 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")) ^
--- 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
--- 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 *)
--- 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
--- 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 *)
--- 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 ();;
--- 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;
--- 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);
--- 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");
--- 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
);
--- 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 ();
--- 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
--- 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))
--- 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
--- 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;
--- 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
--- 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)
--- 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
--- 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);
--- 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;
--- 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
--- 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
--- 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)
--- 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
--- 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 =
--- 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;
--- 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
--- 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 ();