diff -r 4e6fc3336336 -r 07a042166900 src/Tools/isac/MathEngBasic/rewrite.sml
--- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:53:17 2020 +0200
+++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 22 11:06:48 2020 +0200
@@ -3,33 +3,38 @@
 *)
 
 signature REWRITE =
-  sig
-    val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
-    val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
-    val eval_prog_expr: theory -> Rule_Set.T -> term -> term
-    val eval_true_: theory -> Rule_Set.T -> term -> bool
-    val eval_true: theory -> term list -> Rule_Set.T -> bool
-    val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
-      -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
-    val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
-      term -> (term * term list) option
-    val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
-      -> (term * term) list -> thm -> term -> (term * term list) option
-    val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
-    val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
-    val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
-      -> term -> (term * term list) option
+sig
+  val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
+  val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
+  val eval_prog_expr: theory -> Rule_Set.T -> term -> term
+  val eval_true_: theory -> Rule_Set.T -> term -> bool
+  val eval_true: theory -> term list -> Rule_Set.T -> bool
+  val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
+    -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
+  val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
+    term -> (term * term list) option
+  val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
+    -> (term * term) list -> thm -> term -> (term * term list) option
+  val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
+  val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
+  val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
+    -> term -> (term * term list) option
+
+  val trace_on: bool Unsynchronized.ref
+  val depth: int Unsynchronized.ref
+  val lim_deriv: int Unsynchronized.ref
+
 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   (* NONE *)
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
-    val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
-      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
-    val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
-    val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
-    val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
-    val trace1: int -> string -> unit
+  val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
+    Rule_Set.T -> bool -> thm -> term -> (term * term list) option
+  val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
+  val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
+  val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
+  val trace1: int -> string -> unit
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
-  end
+end
 
 (**)
 structure Rewrite(**): REWRITE(**) =
@@ -39,10 +44,16 @@
 exception NO_REWRITE;
 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
 
+val trace_on = Unsynchronized.ref false;
+(* depth of recursion in traces of the rewriter, if trace_on:=true *)
+val depth = Unsynchronized.ref 99999;
+(* no of rewrites exceeding this int -> NO rewrite *)
+val lim_deriv = Unsynchronized.ref 100;
+
 fun trace i str = 
-  if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else ()
+  if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
 fun trace1 i str = 
-  if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else ()
+  if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
 
 fun rewrite__ thy i bdv tless rls put_asm thm ct =
   let
@@ -58,7 +69,7 @@
     val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
     val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
     val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
-    val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
+    val _ = if ! trace_on andalso i < ! depth andalso p' <> []
 	    then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
     val (t'', p'') =                                                     (*conditional rewriting*)
       let
@@ -66,20 +77,20 @@
 	    in
 	      if nofalse
         then
-          (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
+          (if ! trace_on andalso i < ! depth andalso p' <> []
           then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
   	        "   stored: " ^ UnparseC.terms_in_thy thy simpl_p')
   	      else();
           (t',simpl_p'))                                               (* uncond.rew. from above*)
         else 
-          (if ! Trace.trace_rewrite andalso i < ! Trace.depth 
+          (if ! trace_on andalso i < ! depth 
           then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
           else();
           raise STOP_REW_SUB (* don't go into subterms of cond *))
 	    end
     in
       if TermC.perm lhs rhs andalso not (tless bdv (t', t))                        (*ordered rewriting*)
-      then (if ! Trace.trace_rewrite andalso i < ! Trace.depth 
+      then (if ! trace_on andalso i < ! depth 
   	    then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
   	    else (); 
   	    raise NO_REWRITE)