1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 12:39:26 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 15:56:15 2020 +0200
1.3 @@ -155,7 +155,7 @@
1.4 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.5 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.6 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.7 - ThmC_Def.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 @@ -169,7 +169,7 @@
1.13 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.14 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.15 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.16 - ThmC_Def.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