1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -154,13 +154,13 @@
     1.4  (*/------- this will disappear eventually -----------\*)
     1.5  type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
     1.6    (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
     1.7 -val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
     1.8 +val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
     1.9  local
    1.10      fun ii (_: term) = e_rrlsstate;
    1.11 -    fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
    1.12 -    fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
    1.13 +    fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
    1.14 +    fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
    1.15      fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
    1.16 -    fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
    1.17 +    fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
    1.18  in
    1.19  val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
    1.20  		  next_rule = ne, attach_form = fo};