1.1 --- a/src/sml/Scripts/rewrite.sml	Mon Mar 09 12:14:56 2009 +0100
     1.2 +++ b/src/sml/Scripts/rewrite.sml	Wed Aug 19 10:21:06 2009 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  (*17.6.00: rewrite by going down the term with rew_sub*)
     1.6  (* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
     1.7 -       (thy, 1, [], rew_ord, erls, bool, thm, term);
     1.8 +       (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
     1.9     *)
    1.10  fun rewrite__ thy i bdv tless rls put_asm thm ct =
    1.11    ((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*)
    1.12 @@ -34,6 +34,9 @@
    1.13  	(((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
    1.14     val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    1.15         (thy, 1, [],  ord,   erls,false,   [],  r, t);
    1.16 +   val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    1.17 +       (thy, i, bdv, tless, rls, put_asm, [],  
    1.18 +	((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct);
    1.19     *)
    1.20  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    1.21    ((*TODO.new_c:( *)(*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
    1.22 @@ -269,6 +272,8 @@
    1.23  (*.rewriting without internal argument [] for rew_ord.*)
    1.24  (* val (thy, rew_ord, erls, bool, thm, term) =
    1.25         (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
    1.26 +   val (thy, rew_ord, erls, bool, thm, term) =
    1.27 +       (thy, rew_ord, erls, false, thm, t'');
    1.28     *)
    1.29  fun rewrite_ thy rew_ord erls bool thm term = 
    1.30      rewrite__ thy 1 [] rew_ord erls bool thm term;

     2.1 --- a/src/smltest/IsacKnowledge/algein.sml	Mon Mar 09 12:14:56 2009 +0100
     2.2 +++ b/src/smltest/IsacKnowledge/algein.sml	Wed Aug 19 10:21:06 2009 +0200
     2.3 @@ -136,7 +136,7 @@
     2.4  val t = str2term "0 = 0";
     2.5  val Some (t',_) = rewrite_ thy rew_ord erls false thm t;
     2.6  term2str t';
     2.7 -(*"0 = ?z1 * 0"*)
     2.8 +(********"0 = ?z1 * 0"*)
     2.9  
    2.10  (*testing code in ME/appl.sml*)
    2.11  val sube = ["?z1 = 3"];
    2.12 @@ -146,10 +146,10 @@
    2.13  
    2.14  val t'' = subst_atomic subst t';
    2.15  term2str t'';
    2.16 -(*"0 = 3 * 0"*)
    2.17 +(********"0 = 3 * 0"*)
    2.18  
    2.19  val thm = assoc_thm' thy ("sym","");
    2.20 -(*----- GOON Widerspruch 3 = 777
    2.21 +(*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
    2.22  val Some (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    2.23  *)
    2.24