1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Tue Aug 17 22:50:20 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 18 11:35:24 2021 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4     (c) due to copyright terms
     1.5  
     1.6  In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access.
     1.7 -*)
     1.8 +*)                                       
     1.9  signature RULE_SET =
    1.10  sig
    1.11    datatype T = datatype Rule_Def.rule_set
    1.12 @@ -14,6 +14,7 @@
    1.13      preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
    1.14  
    1.15    val append_rules: string -> T -> Rule_Def.rule list -> T
    1.16 +  val append_erls_rules: string -> T -> Rule_Def.rule list -> T
    1.17    val keep_unique_rules: string -> T ->  Rule_Def.rule list -> T
    1.18    val merge: string -> T -> T -> T
    1.19    val get_rules: T -> Rule_Def.rule list
    1.20 @@ -60,7 +61,9 @@
    1.21        calc = calc, rules = rules, scr = scr}
    1.22    | rep (Rule_Def.Rrls _)  = rep empty
    1.23  
    1.24 -fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
    1.25 +fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *)
    1.26 +    Rule_Def.Repeat {id = id, preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty, 
    1.27 +      srls = Rule_Def.Empty, calc = [], rules = r, errpatts = [], scr = Rule_Def.Empty_Prog}
    1.28    | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
    1.29  			rules = rs, errpatts = errpatts, scr = sc}) r =
    1.30      Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
    1.31 @@ -71,6 +74,21 @@
    1.32        rules = rs @ r, errpatts = errpatts, scr = sc}
    1.33    | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
    1.34  
    1.35 +fun append_erls_rules id_erls Rule_Def.Empty _ =
    1.36 +    raise ERROR ("append_erls_rules: with \"" ^ id_erls ^ "\" not for Rule_Def.Empty")
    1.37 +  | append_erls_rules id_erls (Rule_Def.Repeat 
    1.38 +    {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca,
    1.39 +			rules = rules, errpatts = errpatts, scr = sc}) rs =
    1.40 +    Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs, 
    1.41 +      srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc}
    1.42 +  | append_erls_rules id_erls (Rule_Def.Sequence
    1.43 +    {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca,
    1.44 +			rules = rules, errpatts = errpatts, scr = sc}) rs =
    1.45 +    Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs,
    1.46 +      srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc}
    1.47 +  | append_erls_rules id_erls (Rule_Def.Rrls _) _ =
    1.48 +    raise ERROR ("append_erls_rules: not for reverse-rewrite-rule-set " ^ id_erls);
    1.49 +
    1.50  fun merge_ids rls1 rls2 =
    1.51    let 
    1.52      val id1 = (#id o rep) rls1