1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 13:13:07 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 13:27:55 2020 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4                    ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
     1.5                  NONE => rew_once ruls asm ct apno thms
     1.6                | SOME (ct', asm') => 
     1.7 -                (trace1 i (" rewrites to: " ^ UnparseC.term_thy thy ct');
     1.8 +                (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
     1.9                  rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
    1.10                  (* once again try the same rule, e.g. associativity against "()"*)
    1.11            | Rule.Num_Calc (cc as (op_, _)) => 
    1.12 @@ -554,8 +554,8 @@
    1.13                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
    1.14                      ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
    1.15                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 
    1.16 -                    Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
    1.17 -                  val _ = trace1 i (" calc. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
    1.18 +                    Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.19 +                  val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.20                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.21              end
    1.22            | Rule.Cal1 (cc as (op_, _)) => 
    1.23 @@ -568,8 +568,8 @@
    1.24                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
    1.25                      ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
    1.26                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
    1.27 -                     Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
    1.28 -                  val _ = trace1 i (" cal1. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
    1.29 +                     Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.30 +                  val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.31                  in the pairopt end
    1.32              end
    1.33            | Rule.Rls_ rls' => 
    1.34 @@ -578,7 +578,7 @@
    1.35              | NONE => rew_once ruls asm ct apno thms)
    1.36            | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
    1.37        val ruls = (#rules o Rule.Rule_Set.rep) rls;
    1.38 -(*    val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_thy thy ct)*)
    1.39 +(*    val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
    1.40        val (ct', asm') = rew_once ruls [] ct Noap ruls;
    1.41  "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
    1.42    = (ruls, []:term list, ct, Noap, ruls);