src/FOLP/simp.ML
changeset 32091 30e2ffbba718
parent 30190 479806475f3c
child 32449 696d64ed85da
     1.1 --- a/src/FOLP/simp.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4    let fun norm thm = 
     1.5        case lhs_of(concl_of thm) of
     1.6            Const(n,_)$_ => n
     1.7 -        | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
     1.8 +        | _ => error "No constant in lhs of a norm_thm"
     1.9    in map norm normE_thms end;
    1.10  
    1.11  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    1.12 @@ -122,7 +122,7 @@
    1.13  val refl_tac = resolve_tac refl_thms;
    1.14  
    1.15  fun find_res thms thm =
    1.16 -    let fun find [] = (Display.prths thms; error"Check Simp_Data")
    1.17 +    let fun find [] = error "Check Simp_Data"
    1.18            | find(th::thms) = thm RS th handle THM _ => find thms
    1.19      in find thms end;
    1.20  
    1.21 @@ -249,8 +249,8 @@
    1.22  fun insert_thm_warn th net = 
    1.23    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    1.24    handle Net.INSERT => 
    1.25 -    (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
    1.26 -     net);
    1.27 +    (writeln ("Duplicate rewrite or congruence rule:\n" ^
    1.28 +        Display.string_of_thm_without_context th); net);
    1.29  
    1.30  val insert_thms = fold_rev insert_thm_warn;
    1.31  
    1.32 @@ -275,8 +275,8 @@
    1.33  fun delete_thm_warn th net = 
    1.34    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    1.35    handle Net.DELETE => 
    1.36 -    (writeln"\nNo such rewrite or congruence rule:";  Display.print_thm th;
    1.37 -     net);
    1.38 +    (writeln ("No such rewrite or congruence rule:\n" ^
    1.39 +        Display.string_of_thm_without_context th); net);
    1.40  
    1.41  val delete_thms = fold_rev delete_thm_warn;
    1.42  
    1.43 @@ -290,9 +290,9 @@
    1.44  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.45  let fun find((p as (th,ths))::ps',ps) =
    1.46            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.47 -      | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    1.48 -                           Display.print_thm thm;
    1.49 -                           ([],simps'))
    1.50 +      | find([],simps') =
    1.51 +          (writeln ("No such rewrite or congruence rule:\n" ^
    1.52 +              Display.string_of_thm_without_context thm); ([], simps'))
    1.53      val (thms,simps') = find(simps,[])
    1.54  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.55        simps = simps', simp_net = delete_thms thms simp_net }
    1.56 @@ -311,8 +311,9 @@
    1.57  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
    1.58  
    1.59  fun print_ss(SS{congs,simps,...}) =
    1.60 -        (writeln"Congruences:"; Display.prths congs;
    1.61 -         writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
    1.62 +  writeln (cat_lines
    1.63 +   (["Congruences:"] @ map Display.string_of_thm_without_context congs @
    1.64 +    ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
    1.65  
    1.66  
    1.67  (* Rewriting with conditionals *)
    1.68 @@ -435,7 +436,8 @@
    1.69          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
    1.70          val anet' = List.foldr lhs_insert_thm anet rwrls
    1.71      in  if !tracing andalso not(null new_rws)
    1.72 -        then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    1.73 +        then writeln (cat_lines
    1.74 +          ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
    1.75          else ();
    1.76          (ss,thm,anet',anet::ats,cs) 
    1.77      end;