1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Sep 27 13:35:06 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 07:28:10 2010 +0200
     1.3 @@ -272,30 +272,30 @@
     1.4    in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
     1.5    (*end*);
     1.6  
     1.7 -(* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);
     1.8 -   *)
     1.9 -(*.rewrite using a list of terms.*)
    1.10 -fun rewrite_terms_ thy ord erls subte t =
    1.11 -    let (*val _=tracing("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
    1.12 -		      term_detail2str (hd subte)^
    1.13 +(* given a list of equalities (lhs = rhs) and a term, 
    1.14 +   replace all occurrences of lhs in the term with rhs;
    1.15 +   thus the order or equalities matters: put variables in lhs first. *)
    1.16 +fun rewrite_terms_ thy ord erls equs t =
    1.17 +    let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^
    1.18 +		      term_detail2str (hd equs)^
    1.19  		      "### rewrite_terms_ t= '"^term2str t^"' ..."^
    1.20  		      term_detail2str t);*)
    1.21  	fun rew_ (t', asm') [] _ = (t', asm')
    1.22 -	  (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);
    1.23 +	  (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t);
    1.24  	     2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
    1.25  	     rew_ (t', asm') (r::rs) t;
    1.26  	     *)
    1.27  	  | rew_ (t', asm') (rules as r::rs) t =
    1.28  	    let val _ = tracing("rew_ "^term2str t);
    1.29  		val (t'', asm'', lrd, rew) = 
    1.30 -		    rew_sub thy 1 [] ord erls false [] r t
    1.31 +		    rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
    1.32  	    in if rew 
    1.33 -	       then (tracing("true  rew_ "^term2str t'');
    1.34 +	       then (tracing ("true  rew_ " ^ term2str t'');
    1.35  		   rew_ (t'', asm' @ asm'') rules t'')
    1.36 -	       else (tracing("false rew_ "^term2str t'');
    1.37 +	       else (tracing ("false rew_ " ^ term2str t'');
    1.38  		   rew_ (t', asm') rs t')
    1.39  	    end
    1.40 -	val (t'', asm'') = rew_ (e_term, []) subte t
    1.41 +	val (t'', asm'') = rew_ (e_term, []) equs t
    1.42      in if t'' = e_term 
    1.43         then NONE else SOME (t'', asm'')
    1.44      end;