--- a/src/FOLP/simp.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/FOLP/simp.ML Tue Jul 21 01:03:18 2009 +0200
@@ -113,7 +113,7 @@
let fun norm thm =
case lhs_of(concl_of thm) of
Const(n,_)$_ => n
- | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
+ | _ => 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
@@ -122,7 +122,7 @@
val refl_tac = resolve_tac refl_thms;
fun find_res thms thm =
- let fun find [] = (Display.prths thms; error"Check Simp_Data")
+ let fun find [] = error "Check Simp_Data"
| find(th::thms) = thm RS th handle THM _ => find thms
in find thms end;
@@ -249,8 +249,8 @@
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:"; Display.print_thm th;
- net);
+ (writeln ("Duplicate rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val insert_thms = fold_rev insert_thm_warn;
@@ -275,8 +275,8 @@
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:"; Display.print_thm th;
- net);
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val delete_thms = fold_rev delete_thm_warn;
@@ -290,9 +290,9 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
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:";
- Display.print_thm thm;
- ([],simps'))
+ | find([],simps') =
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context thm); ([], simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
simps = simps', simp_net = delete_thms thms simp_net }
@@ -311,8 +311,9 @@
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
fun print_ss(SS{congs,simps,...}) =
- (writeln"Congruences:"; Display.prths congs;
- writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
+ writeln (cat_lines
+ (["Congruences:"] @ map Display.string_of_thm_without_context congs @
+ ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
(* Rewriting with conditionals *)
@@ -435,7 +436,8 @@
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
val anet' = List.foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
- then (writeln"Adding rewrites:"; Display.prths new_rws; ())
+ then writeln (cat_lines
+ ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
else ();
(ss,thm,anet',anet::ats,cs)
end;