1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue Oct 22 17:38:34 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Oct 24 00:02:29 2013 +0100
     1.3 @@ -536,16 +536,24 @@
     1.4             then
     1.5  	           if f = f_ then Ass (m,f') else AssWeak (m,f')
     1.6  	         else NotAss
     1.7 -       | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)  => 
     1.8 -	         if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)
     1.9 -           then
    1.10 -	           if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.11 -	         else NotAss
    1.12 +       | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)  =>
    1.13 +           let
    1.14 +             val thy = ML_Context.the_generic_context () |> Context.theory_of;
    1.15 +           in
    1.16 +             if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.17 +             then
    1.18 +               if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.19 +             else NotAss
    1.20 +           end
    1.21         | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
    1.22 -	         if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)
    1.23 -           then
    1.24 -	           if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.25 -	         else NotAss
    1.26 +           let
    1.27 +             val thy = ML_Context.the_generic_context () |> Context.theory_of;
    1.28 +           in
    1.29 +             if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.30 +             then
    1.31 +               if f = f_ then Ass (m,f') else AssWeak (m,f')
    1.32 +             else NotAss
    1.33 +           end
    1.34         | _ => NotAss)
    1.35  
    1.36    | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))