1.1 --- a/src/sml/Scripts/rewrite.sml	Mon Dec 10 11:09:26 2007 +0100
     1.2 +++ b/src/sml/Scripts/rewrite.sml	Mon Dec 10 14:18:49 2007 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4       val (lhs,rhs) = (dest_equals' o strip_trueprop 
     1.5  		      o Logic.strip_imp_concl) r;
     1.6       val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
     1.7 -       (*TODOtest: (-"-) handle _ => raise NO_REWRITE; 12.8.02 ???*)
     1.8 +       (*TODOtest: (-"-) handle MATCH => raise NO_REWRITE; 12.8.02 ???*)
     1.9       (*val _=writeln("@@@ rew_sub: Pattern.match (lhs,t) ");*)
    1.10       val r' = ren_inst (insts, r, lhs, t);
    1.11       val p' = map strip_trueprop (Logic.strip_imp_prems r'); 
    1.12 @@ -58,7 +58,7 @@
    1.13  	    else 
    1.14  		(if ! trace_rewrite andalso i < ! depth 
    1.15  		 then writeln((idt"#"(i+1))^" asms false: "^(terms2str p')) 
    1.16 -		 else(); raise STOP_REW_SUB)
    1.17 +		 else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
    1.18  	 end
    1.19     in if perm lhs rhs andalso not (tless bdv (t',t)) 
    1.20  	then (if ! trace_rewrite andalso i < ! depth 
    1.21 @@ -70,7 +70,7 @@
    1.22  		      ", p'' ="^(terms2str p'')^", true)");*)
    1.23  	      (t'',p'',[],true))
    1.24     end) handle STOP_REW_SUB => (t,[],[],false)
    1.25 -   ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests*) => 
    1.26 +   ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) => 
    1.27       ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
    1.28        case t of
    1.29  	Const(s,T) => (Const(s,T),[],lrd,false)

     2.1 --- a/src/smltest/Scripts/term_G.sml	Mon Dec 10 11:09:26 2007 +0100
     2.2 +++ b/src/smltest/Scripts/term_G.sml	Mon Dec 10 14:18:49 2007 +0100
     2.3 @@ -80,3 +80,4 @@
     2.4  (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) 
     2.5  handle MATCH => ([(* (Term.indexname * Term.typ) *)],
     2.6  		 [(* (Term.indexname * Term.term) *)]);
     2.7 +Pattern.MATCH;