src/Tools/isac/Interpret/script.sml
changeset 55443 46613d0a9fc9
parent 55432 1780e9905d80
child 59184 831fa972f73b
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Jun 12 21:59:15 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Jun 13 09:55:49 2014 +0200
     1.3 @@ -534,7 +534,7 @@
     1.4  	         else NotAss
     1.5         | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)  =>
     1.6             let
     1.7 -             val thy = ML_Context.the_generic_context () |> Context.theory_of;
     1.8 +             val thy = assoc_thy "Isac";
     1.9             in
    1.10               if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.11               then
    1.12 @@ -543,7 +543,7 @@
    1.13             end
    1.14         | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
    1.15             let
    1.16 -             val thy = ML_Context.the_generic_context () |> Context.theory_of;
    1.17 +             val thy = assoc_thy "Isac";
    1.18             in
    1.19               if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
    1.20               then