1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -371,25 +371,25 @@
     1.4          val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.5  	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
     1.6  
     1.7 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _)) =
     1.8 +val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _)) =
     1.9             LI.find_next_step sc (pt, pos) ist ctxt (*of*);
    1.10  "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
    1.11    = (sc, (pt, pos), ist, ctxt);
    1.12  
    1.13 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
    1.14 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
    1.15    (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
    1.16  "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
    1.17    = ((prog, (ptp, ctxt)), (Pstate ist));
    1.18    (*if*) path = [] (*then*);
    1.19  
    1.20 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
    1.21 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
    1.22              scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
    1.23  "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
    1.24    = (cc, (trans_scan_dn ist), (Program.body_of prog));
    1.25      (*if*) Tactical.contained_in t (*else*);
    1.26        val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);
    1.27  
    1.28 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
    1.29 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
    1.30            check_tac cc ist (prog_tac, form_arg)  (*return from xxx*);
    1.31  "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
    1.32    = (check_tac cc ist (prog_tac, form_arg));