1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Thu Apr 23 09:29:56 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Thu Apr 23 12:34:54 2020 +0200
     1.3 @@ -17,6 +17,8 @@
     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  
    1.10    type for_kestore
    1.11    val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
    1.12 @@ -151,11 +153,14 @@
    1.13    | get_rules (Rule_Def.Sequence {rules, ...}) = rules
    1.14    | get_rules (Rule_Def.Rrls _) = [];
    1.15  
    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  (*/------- this will disappear eventually -----------\*)
    1.20  type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
    1.21    (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
    1.22  val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
    1.23 -local
    1.24 +local           
    1.25      fun ii (_: term) = e_rrlsstate;
    1.26      fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
    1.27      fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];