1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 22:08:01 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 18 18:15:27 2021 +0200
     1.3 @@ -62,7 +62,6 @@
     1.4  fun trace_eq2 i str thy t t' =
     1.5    trace i (" " ^ str ^ ": \"" ^
     1.6      UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
     1.7 -
     1.8  fun trace1 i str =
     1.9    if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
    1.10  fun trace_in1 i str thmid =
    1.11 @@ -99,9 +98,9 @@
    1.12        let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls 	     
    1.13  	    in
    1.14  	      if nofalse
    1.15 -        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
    1.16 +        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
    1.17          else (trace_in5 i "asms false" thy p'; raise NO_REWRITE)   (* don't go into subtm.of cond*)
    1.18 -	    end
    1.19 +	    end                                    
    1.20    in
    1.21      if TermC.perm lhs rhs andalso not (tless bdv (t', t))                     (*ordered rewriting*)
    1.22      then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
    1.23 @@ -124,7 +123,7 @@
    1.24            let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
    1.25            in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
    1.26      end)
    1.27 -and eval__true thy i asms bdv rls =           (* simplify asumptions until one evaluates to false*)
    1.28 +and eval__true thy i asms bdv rls =            (* rewrite asumptions until one evaluates to false*)
    1.29    if asms = [@{term True}] orelse asms = [] then ([], true)
    1.30    else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
    1.31      if asms = [@{term False}] then ([], false)
    1.32 @@ -140,7 +139,7 @@
    1.33              (*asm false .. thm not applied ^^^; continue until False vvv*)
    1.34              else chk (indets @ [t] @ a') asms);
    1.35        in chk [] asms end
    1.36 -and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                          (* rewrite with a rule set*)
    1.37 +and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)
    1.38      raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
    1.39    | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)
    1.40      let
    1.41 @@ -251,10 +250,10 @@
    1.42          end
    1.43      end;
    1.44  
    1.45 -(* rewriting without argument [] for rew_ord;  WN110603: shouldnt asm<>[] lead to false? *)
    1.46 +(* rewriting without argument [] for rew_ord *)
    1.47  fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
    1.48  
    1.49 -(* rewriting without internal argument [] *)
    1.50 +(* rewriting without internal arguments 1, [] *)
    1.51  fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
    1.52  fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
    1.53