1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 29 09:03:01 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 29 12:30:51 2020 +0200
     1.3 @@ -525,9 +525,9 @@
     1.4    = (thy, 1, bool, []:(term * term) list, rls, term);
     1.5  
     1.6  (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
     1.7 -      datatype switch = Appl | Noap;
     1.8 +      datatype switch = Applicable.Yes | Noap;
     1.9        fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
    1.10 -        | rew_once ruls asm ct Appl [] = 
    1.11 +        | rew_once ruls asm ct Applicable.Yes [] = 
    1.12            (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
    1.13            | Rule_Set.Sequence _ => (ct, asm)
    1.14            | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
    1.15 @@ -540,7 +540,7 @@
    1.16                  NONE => rew_once ruls asm ct apno thms
    1.17                | SOME (ct', asm') => 
    1.18                  (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
    1.19 -                rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
    1.20 +                rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
    1.21                  (* once again try the same rule, e.g. associativity against "()"*)
    1.22            | Rule.Eval (cc as (op_, _)) => 
    1.23              let val _= trace1 i (" try calc: " ^ op_ ^ "'")
    1.24 @@ -554,7 +554,7 @@
    1.25                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 
    1.26                      ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.27                    val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.28 -                in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.29 +                in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
    1.30              end
    1.31            | Rule.Cal1 (cc as (op_, _)) => 
    1.32              let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
    1.33 @@ -572,7 +572,7 @@
    1.34              end
    1.35            | Rule.Rls_ rls' => 
    1.36              (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
    1.37 -              SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
    1.38 +              SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
    1.39              | NONE => rew_once ruls asm ct apno thms)
    1.40            | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
    1.41        val ruls = (#rules o Rule.Rule_Set.rep) rls;