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;