1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Apr 09 18:21:09 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Fri Apr 10 12:28:47 2020 +0200
     1.3 @@ -90,11 +90,11 @@
     1.4    list
     1.5  
     1.6  fun trta2str (t, r, (t', a)) =
     1.7 -  "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule_Set.rule2str' r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
     1.8 +  "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
     1.9  fun trtas2str trtas = (strs2str o (map trta2str)) trtas
    1.10  val deriv2str = trtas2str
    1.11  fun rta2str (r, (t, a)) =
    1.12 -  "\n(" ^ Rule_Set.rule2str' r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
    1.13 +  "\n(" ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
    1.14  fun rtas2str rtas = (strs2str o (map rta2str)) rtas
    1.15  val deri2str = rtas2str
    1.16  
    1.17 @@ -186,7 +186,7 @@
    1.18            (case Rewrite.rewrite_set_ thy true rls t of
    1.19              NONE => rew_once lim rts t apno rs'
    1.20            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
    1.21 -        | rule => error ("rew_once: uncovered case " ^ Rule_Set.rule2str rule))
    1.22 +        | rule => error ("rew_once: uncovered case " ^ Rule.rule2str rule))
    1.23      | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
    1.24    in rew_once (! Celem.lim_deriv) [] tt Noap rs end
    1.25  
    1.26 @@ -222,7 +222,7 @@
    1.27      | _ => "sym_" ^ thmID
    1.28    in Rule.Thm (thmID', thm') end
    1.29  | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
    1.30 -| sym_rule r = error ("sym_rule: not for " ^  Rule_Set.rule2str r)
    1.31 +| sym_rule r = error ("sym_rule: not for " ^  Rule.rule2str r)
    1.32  
    1.33  (*version for reverse rewrite used before 040214*)
    1.34  fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
    1.35 @@ -233,7 +233,7 @@
    1.36    | eq_Thm (Rule.Thm (_, _), _) = false
    1.37    | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.rls2str r1 = Rule_Set.rls2str r2
    1.38    | eq_Thm (Rule.Rls_ _, _) = false
    1.39 -  | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule_Set.rule2str r1 ^ "' '" ^ Rule_Set.rule2str r2 ^ "'")
    1.40 +  | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.rule2str r1 ^ "' '" ^ Rule.rule2str r2 ^ "'")
    1.41  fun distinct_Thm r = gen_distinct eq_Thm r
    1.42  
    1.43  fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC.id_of_thm thm))