diff -r 63cecf440235 -r 40eb8aa2b0d6 src/Tools/isac/MathEngBasic/rewrite.sml
--- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 22:08:01 2021 +0200
+++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 18 18:15:27 2021 +0200
@@ -62,7 +62,6 @@
 fun trace_eq2 i str thy t t' =
   trace i (" " ^ str ^ ": \"" ^
     UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
-
 fun trace1 i str =
   if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
 fun trace_in1 i str thmid =
@@ -99,9 +98,9 @@
       let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls 	     
 	    in
 	      if nofalse
-        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
+        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
         else (trace_in5 i "asms false" thy p'; raise NO_REWRITE)   (* don't go into subtm.of cond*)
-	    end
+	    end                                    
   in
     if TermC.perm lhs rhs andalso not (tless bdv (t', t))                     (*ordered rewriting*)
     then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
@@ -124,7 +123,7 @@
           let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
           in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
     end)
-and eval__true thy i asms bdv rls =           (* simplify asumptions until one evaluates to false*)
+and eval__true thy i asms bdv rls =            (* rewrite asumptions until one evaluates to false*)
   if asms = [@{term True}] orelse asms = [] then ([], true)
   else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
     if asms = [@{term False}] then ([], false)
@@ -140,7 +139,7 @@
             (*asm false .. thm not applied ^^^; continue until False vvv*)
             else chk (indets @ [t] @ a') asms);
       in chk [] asms end
-and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                          (* rewrite with a rule set*)
+and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)
     raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
   | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)
     let
@@ -251,10 +250,10 @@
         end
     end;
 
-(* rewriting without argument [] for rew_ord;  WN110603: shouldnt asm<>[] lead to false? *)
+(* rewriting without argument [] for rew_ord *)
 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
 
-(* rewriting without internal argument [] *)
+(* rewriting without internal arguments 1, [] *)
 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;