1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -552,7 +552,7 @@
     1.4                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
     1.5                      ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
     1.6                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 
     1.7 -                    Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
     1.8 +                    ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
     1.9                    val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.10                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.11              end
    1.12 @@ -566,7 +566,7 @@
    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_in_thy thy ct ^ " = NONE")
    1.17 +                     ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.18                    val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.19                  in the pairopt end
    1.20              end