1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 15:42:50 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:16:11 2020 +0200
     1.3 @@ -40,9 +40,9 @@
     1.4  exception STOP_REW_SUB; (*WN050820 quick and dirty*)
     1.5  
     1.6  fun trace i str = 
     1.7 -  if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
     1.8 +  if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else ()
     1.9  fun trace1 i str = 
    1.10 -  if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
    1.11 +  if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else ()
    1.12  
    1.13  fun rewrite__ thy i bdv tless rls put_asm thm ct =
    1.14    let
    1.15 @@ -58,7 +58,7 @@
    1.16      val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
    1.17      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
    1.18      val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
    1.19 -    val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
    1.20 +    val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
    1.21  	    then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
    1.22      val (t'', p'') =                                                     (*conditional rewriting*)
    1.23        let
    1.24 @@ -66,20 +66,20 @@
    1.25  	    in
    1.26  	      if nofalse
    1.27          then
    1.28 -          (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
    1.29 +          (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
    1.30            then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
    1.31    	        "   stored: " ^ UnparseC.terms_in_thy thy simpl_p')
    1.32    	      else();
    1.33            (t',simpl_p'))                                               (* uncond.rew. from above*)
    1.34          else 
    1.35 -          (if ! Celem.trace_rewrite andalso i < ! Celem.depth 
    1.36 +          (if ! Trace.trace_rewrite andalso i < ! Trace.depth 
    1.37            then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
    1.38            else();
    1.39            raise STOP_REW_SUB (* don't go into subterms of cond *))
    1.40  	    end
    1.41      in
    1.42        if TermC.perm lhs rhs andalso not (tless bdv (t', t))                        (*ordered rewriting*)
    1.43 -      then (if ! Celem.trace_rewrite andalso i < ! Celem.depth 
    1.44 +      then (if ! Trace.trace_rewrite andalso i < ! Trace.depth 
    1.45    	    then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
    1.46    	    else (); 
    1.47    	    raise NO_REWRITE)