1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Sun Sep 22 17:28:55 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Sun Sep 22 18:09:05 2013 +0200
     1.3 @@ -546,6 +546,9 @@
     1.4  ruleset' := overwritelthy thy (!ruleset',
     1.5    [("list_rls",list_rls)
     1.6     ]);
     1.7 +*}
     1.8 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
     1.9 +ML {*
    1.10  
    1.11  (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
    1.12  val tless_true = dummy_ord;
    1.13 @@ -642,7 +645,7 @@
    1.14  			   Calc ("Tools.matches",eval_matches "#matches")
    1.15  			   ] (*i.A. zu viele rules*)
    1.16  			  );*)
    1.17 -(* val atools_erls = prep_rls(
    1.18 +(* val atools_erls = prep_rls(     (*outcommented*)
    1.19    Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), 
    1.20        erls = e_rls, srls = Erls, calc = [], errpatts = [],
    1.21        rules = [Thm ("refl",num_str @{thm refl}),
    1.22 @@ -667,7 +670,7 @@
    1.23  	       ],
    1.24        scr = Prog ((term_of o the o (parse @{theory})) "empty_script")
    1.25        }:rls);
    1.26 -ruleset' := overwritelth @{theory} 
    1.27 +ruleset' := overwritelth @{theory} (*outcommented*)
    1.28  		(!ruleset',
    1.29  		 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
    1.30  		  ]);
    1.31 @@ -711,5 +714,6 @@
    1.32  	      list_rls);
    1.33  ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
    1.34  *}
    1.35 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
    1.36  
    1.37  end