1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Nov 24 14:33:42 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed Nov 30 12:09:24 2016 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4  > *** dropwhile': did not start with equal elements*)
     1.5  
     1.6  (*040214: version for concat_deriv*)
     1.7 -fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
     1.8 +fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
     1.9  
    1.10  fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) = 
    1.11        (Rewrite (id, thm), 
    1.12 @@ -438,8 +438,8 @@
    1.13      fun derivat ([]:(term * rule * (term * term list)) list) = e_term
    1.14        | derivat dt = (#1 o #3 o last_elem) dt
    1.15      fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
    1.16 -    val  fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo
    1.17 -    val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
    1.18 +    val  fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo
    1.19 +    val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
    1.20    in 
    1.21      case (fod, ifod) of
    1.22        ([], []) => if fo = ifo then (true, []) else (false, [])
    1.23 @@ -538,7 +538,7 @@
    1.24     (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
    1.25  fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
    1.26    let
    1.27 -    val (_, subst) = get_bdv_subst prog env
    1.28 +    val (_, subst) = Rtools.get_bdv_subst prog env
    1.29      fun scan (_, [], _) = NONE
    1.30        | scan (errpatID, errpat :: errpats, _) =
    1.31            case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
    1.32 @@ -609,7 +609,7 @@
    1.33  fun get_fillpats subst form errpatID thm =
    1.34        let
    1.35          val thmDeriv = Thm.get_name_hint thm
    1.36 -        val (part, thyID) = thy_containing_thm thmDeriv
    1.37 +        val (part, thyID) = Rtools.thy_containing_thm thmDeriv
    1.38          val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    1.39          val Hthm {fillpats, ...} = get_the theID
    1.40          val some = map (get_fillform subst (thm, form) errpatID) fillpats
    1.41 @@ -621,7 +621,7 @@
    1.42      val pp = par_pblobj pt p
    1.43  			    val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
    1.44      val ScrState (env, _, _, _, _, _) = get_istate pt pos
    1.45 -    val subst = get_bdv_subst prog env
    1.46 +    val subst = Rtools.get_bdv_subst prog env
    1.47      val errpatthms = errpats
    1.48        |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
    1.49        |> map (#3: errpat -> thm list)
    1.50 @@ -660,7 +660,7 @@
    1.51          Rewrite_Set rlsID => rlsID
    1.52        | Rewrite_Set_Inst (_, rlsID) => rlsID
    1.53        | _ => "e_rls"
    1.54 -    val (part, thyID) = thy_containing_rls "Isac" rlsID;
    1.55 +    val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
    1.56      val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
    1.57    in case rls of
    1.58          Rls {errpatts, ...} => errpatts