1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -89,14 +89,19 @@
     1.4    (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
     1.5  and rew_sub thy i bdv tless rls put_asm lrd r t = 
     1.6    (let
     1.7 +(** )val _ = @{print}{a = "@ rew_sub: 1 < ?n \<Longrightarrow> NTH ?n..", r = UnparseC.term r};( *TODOO*)
     1.8      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
     1.9 +(** )val _ = @{print}{a = "@ rew_sub NO: patterns..", lhs = UnparseC.term lhs, rhs = UnparseC.term rhs};( *TODOO*)
    1.10      val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
    1.11        handle Pattern.MATCH => raise NO_REWRITE
    1.12 +(** )val _ = @{print}{a = "@ Envir.subst_term: OK gives (3 + - 1)", r' = UnparseC.term r'};( *TODOO*)
    1.13      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
    1.14      val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
    1.15      val _ = trace_in2 i "eval asms" thy r';
    1.16 +(** )val _ = @{print}{a = "@ eval asms", r' = UnparseC.term r'};( *TODOO*)
    1.17      val (t'', p'') =                                                      (*conditional rewriting*)
    1.18        let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls 	     
    1.19 +(** )val _ = @{print}{a = "@ eval__true asms", simpl_p' = UnparseC.terms simpl_p', nofalse = nofalse};( *TODOO*)
    1.20  	    in
    1.21  	      if nofalse
    1.22          then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
    1.23 @@ -140,7 +145,7 @@
    1.24              (*asm false .. thm not applied ^^^; continue until False vvv*)
    1.25              else chk (indets @ [t] @ a') asms);
    1.26        in chk [] asms end
    1.27 -and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                          (* rewrite with a rule set*)
    1.28 +and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)
    1.29      raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
    1.30    | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)
    1.31      let