1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Sep 16 11:28:43 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Sep 16 12:20:00 2013 +0200
     1.3 @@ -585,7 +585,7 @@
     1.4  ML {*
     1.5  (** methods **)
     1.6  store_met
     1.7 - (prep_met (Thy_Info.get_theory "Diff") "met_test" [] e_metID
     1.8 + (prep_met @{theory "Diff"} "met_test" [] e_metID
     1.9   (["Test"],
    1.10     [],
    1.11     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.12 @@ -628,7 +628,6 @@
    1.13  
    1.14  *}
    1.15  ML {*
    1.16 -
    1.17  ruleset' := overwritelthy @{theory} (!ruleset',
    1.18    [("norm_equation", prep_rls norm_equation),
    1.19     ("ac_plus_times", prep_rls ac_plus_times),
    1.20 @@ -1320,7 +1319,7 @@
    1.21  
    1.22  val make_polytest =
    1.23    Rls{id = "make_polytest", preconds = []:term list, 
    1.24 -      rew_ord = ("ord_make_polytest", ord_make_polytest false (Thy_Info.get_theory "Poly")),
    1.25 +      rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
    1.26        erls = testerls, srls = Erls,
    1.27        calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
    1.28  	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),