1.1 --- a/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 18:04:54 2005 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 18:04:54 2005 +0200
     1.3 @@ -106,9 +106,12 @@
     1.4  fun rewrit thm str = 
     1.5      fst (the (rewrite_inst_ Integrate.thy tless_true 
     1.6  			    conditions_in_integration true subs thm str));
     1.7 +(*
     1.8  trace_rewrite := true;
     1.9 +*)
    1.10  val str = rewrit add_new_c (str2t "x ^^^ 2 / 2"); term2s str;
    1.11 -val str = rewrit add_new_c str; term2s str;
    1.12 +val str = (rewrit add_new_c str)
    1.13 +    handle OPTION =>  str2t "no_rewrite";;
    1.14  
    1.15  (*
    1.16  use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";