1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  "----------- step through 'fun rewrite_terms_'  ---------";
     1.5  "----- step 0: args for rewrite_terms_, local fun";
     1.6  val (thy, ord, erls, equs, t) =
     1.7 -    (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
     1.8 +    (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
     1.9       str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
    1.10  "----- step 1: args for rew_";
    1.11  val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
    1.12 @@ -207,21 +207,21 @@
    1.13  "----- step 3: step through rew_sub -- inefficient: goes into subterms";
    1.14  
    1.15  
    1.16 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
    1.17 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
    1.18  writeln "----------- rewrite_terms_  1---------------------------";
    1.19  if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.20  else error "rewrite.sml rewrite_terms_ [x = 0]";
    1.21  
    1.22  val equs = [str2term "M_b 0 = 0"];
    1.23  val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
    1.24 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
    1.25 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
    1.26  writeln "----------- rewrite_terms_  2---------------------------";
    1.27  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.28  else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
    1.29  
    1.30  val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
    1.31  val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
    1.32 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
    1.33 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
    1.34  writeln "----------- rewrite_terms_  3---------------------------";
    1.35  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.36  else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
    1.37 @@ -530,8 +530,8 @@
    1.38        datatype switch = Appl | Noap;
    1.39        fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
    1.40          | rew_once ruls asm ct Appl [] = 
    1.41 -          (case rls of Rule_Set.Rls _ => rew_once ruls asm ct Noap ruls
    1.42 -          | Rule_Set.Seq _ => (ct, asm)
    1.43 +          (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
    1.44 +          | Rule_Set.Seqence _ => (ct, asm)
    1.45            | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
    1.46          | rew_once ruls asm ct apno (rul :: thms) =
    1.47            case rul of
    1.48 @@ -641,7 +641,7 @@
    1.49             chk [] asms;  (*return from eval__true*);
    1.50  "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
    1.51  
    1.52 -(*+*)val Rls {id = "rateq_erls", rules, ...} = rls;
    1.53 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
    1.54  (*+*)(*val rules =
    1.55  (*+*)   [Num_Calc ("Rings.divide_class.divide", fn),
    1.56  (*+*)    Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),