1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Nov 24 14:33:42 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Nov 30 12:09:24 2016 +0100
     1.3 @@ -313,7 +313,7 @@
     1.4  	        else ((*tracing"3### assod ..AssWeak";*) AssWeak(m, f'))
     1.5  	      else ((*tracing"3### assod ..NotAss";*) NotAss)
     1.6      | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ Free (rls_, _) $ _ $ f_) =>
     1.7 -	      if contains_rule (Thm thm'') (assoc_rls rls_)
     1.8 +	      if Rtools.contains_rule (Thm thm'') (assoc_rls rls_)
     1.9          then if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.10  	      else NotAss
    1.11      | _ => NotAss)
    1.12 @@ -333,7 +333,7 @@
    1.13  		         AssWeak (m,f'))
    1.14  	      else ((*tracing"3### assod ..NotAss";*) NotAss))
    1.15      | (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =>
    1.16 -	       if contains_rule (Thm thm'') (assoc_rls rls_)
    1.17 +	       if Rtools.contains_rule (Thm thm'') (assoc_rls rls_)
    1.18           then if f = f_ then Ass (m, f') else AssWeak (m, f')
    1.19  	       else NotAss
    1.20      | _ => NotAss)
    1.21 @@ -366,14 +366,14 @@
    1.22      | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free(rls_,_) $_$f_)  =>
    1.23          let val thy = assoc_thy "Isac";
    1.24          in
    1.25 -          if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.26 +          if Rtools.contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.27            then if f = f_ then Ass (m, f') else AssWeak (m, f')
    1.28            else NotAss
    1.29          end
    1.30      | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
    1.31          let val thy = assoc_thy "Isac";
    1.32          in
    1.33 -          if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.34 +          if Rtools.contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.35            then if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.36            else NotAss
    1.37          end
    1.38 @@ -1208,7 +1208,7 @@
    1.39            (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
    1.40            | _ => error "")
    1.41            (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
    1.42 -      in ((gen_distinct eq_tac) o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
    1.43 +      in ((gen_distinct eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
    1.44  (**)
    1.45  end
    1.46  (**)