1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Mon Apr 27 16:40:11 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Tue Apr 28 15:31:49 2020 +0200
     1.3 @@ -17,8 +17,9 @@
     1.4    val keep_unique_rules: string -> T ->  Rule_Def.rule list -> T
     1.5    val merge: string -> T -> T -> T
     1.6    val get_rules: T -> Rule_Def.rule list
     1.7 -(*val rule2rls' : Rule.rule -> string*)
     1.8 -  val id_from_rule : Rule.rule -> string
     1.9 +(*val rule2rls': Rule.rule -> string*)
    1.10 +  val id_from_rule: Rule.rule -> string
    1.11 +  val contains: Rule.rule -> T -> bool
    1.12  
    1.13    type for_kestore
    1.14    val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
    1.15 @@ -156,6 +157,18 @@
    1.16  fun id_from_rule (Rule.Rls_ rls) = id rls
    1.17    | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
    1.18  
    1.19 +(* check if a rule is contained in a rule-set (recursivley down in Rls_);
    1.20 +   this rule can even be a rule-set itself                             *)
    1.21 +fun contains r rls = 
    1.22 +  let 
    1.23 +    fun (*find (_, Rls_ rls) = finds (get_rules rls)
    1.24 +      | find r12 = equal r12
    1.25 +    and*) finds [] = false
    1.26 +    | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
    1.27 +  in 
    1.28 +    finds (get_rules rls) 
    1.29 +  end
    1.30 +
    1.31  (*/------- this will disappear eventually -----------\*)
    1.32  type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
    1.33    (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);