src/FOLP/simp.ML

 (*Get the norm constants from norm_thms*)
 val norms =
   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
         Const(s,_)$_ => s mem norms | _ => false;
 
 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;
 
 val mk_trans = find_res trans_thms;
 

 
 (*insert a thm in a thm net*)
 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;
 
 fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
 let val thms = mk_simps thm

 
 (*delete a thm from a thm net*)
 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;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
 let val congs' = fold (remove Thm.eq_thm_prop) thms congs

 end;
 
 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 }
 end;
 

 (** Inspection of a simpset **)
 
 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 *)
 
 val (case_thms,case_consts) = split_list case_splits;

         val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
         val new_rws = List.concat(map mk_rew_rules thms);
         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;
 
 fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of