src/Tools/isac/calcelems.sml
changeset 52124 6ce73ec74e8c
parent 52117 d2960738fa09
child 52141 90546fa8b868
     1.1 --- a/src/Tools/isac/calcelems.sml	Fri Sep 20 15:30:09 2013 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sun Sep 22 17:28:55 2013 +0200
     1.3 @@ -485,10 +485,6 @@
     1.4    Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
     1.5      calc = [], errpatts = [], scr=e_rfuns}:rls;
     1.6  
     1.7 -ruleset' := overwritel (!ruleset', 
     1.8 -  [("e_rls", ("Tools", e_rls)),
     1.9 -   ("e_rrls", ("Tools", e_rrls))]);
    1.10 -
    1.11  fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
    1.12    {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
    1.13     (*asm_thm=asm_thm,*)rules=rules,scr=scr}
    1.14 @@ -603,14 +599,6 @@
    1.15      else (Thy_Info.get_theory thy)
    1.16           handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
    1.17  
    1.18 -(*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; WN111014?fun get_rls ?
    1.19 -   these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
    1.20 -   overlays by re-using an identifier in different thys.*)
    1.21 -fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
    1.22 -  handle _ => error ("ME_Isa: '"^rls^"' not in system");
    1.23 -(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
    1.24 -  handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
    1.25 -
    1.26  (*.overwrite an element in an association list and pair it with a thyID
    1.27     in order to create the thy_hierarchy;
    1.28     overwrites existing rls' even if they are defined in a different thy;