ML {*

 "~~~~~ fun xxx, args:"; val () = ();

 *} ML {*

 "-------- test the same called by interSteps norm_Poly -----------";

 "-------- test the same called by interSteps norm_Poly -----------";

 "-------- test the same called by interSteps norm_Poly -----------";

 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";

 writeln(term2str auto_script);

 (*Script Stepwise t_t   =

  (Try (Rewrite_Set discard_minus False) @@

   Try (Rewrite_Set expand_poly_ False) @@

   Try (Repeat (Calculate TIMES)) @@

   Try (Rewrite_Set order_mult_rls_ False) @@

   Try (Rewrite_Set simplify_power_ False) @@

   Try (Rewrite_Set calc_add_mult_pow_ False) @@

   Try (Rewrite_Set reduce_012_mult_ False) @@

   Try (Rewrite_Set order_add_rls_ False) @@

   Try (Rewrite_Set collect_numerals_ False) @@

   Try (Rewrite_Set reduce_012_ False) @@

   Try (Rewrite_Set discard_parentheses1 False))

   ??.empty                                          ..WORKS, NEVERTHELESS *)

 atomty auto_script;

 reset_states ();  

 CalcTree

 [(["Term (b + a - b)", "normalform N"], 

   ("Poly",["polynomial","simplification"],

   ["simplification","for_polynomials"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1;

 show_pt pt;

 (* isabisac17 = 15 [

 (([], Frm), Simplify (b + a - b)),

 (([1], Frm), b + a - b),

 (([1], Res), a),

 (([], Res), a)] *)

 interSteps 1 ([], Res);

 val ((pt,p),_) = get_calc 1;

 show_pt pt;

 (* isabisac17 = 15 [

 (([], Frm), Simplify (b + a - b)),

 (([1], Frm), b + a - b),

 (([1], Res), a),

 (([], Res), a)] *)

 interSteps 1 ([1], Res);

 (*interSteps 1 ([1], Res)<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)

 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));

  val ((pt, p), tacis) = get_calc cI;

 (*if*) (not o is_interpos) ip = false;

 val ip' = lev_pred' pt ip;

 (*Math_Engine.detailstep pt ip      ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)

 "~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);

     val nd = Ctree.get_nd pt p

     val cn = Ctree.children nd;

 (*if*) null cn = true;

 (*if*) (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] = true;

 (*Solve.detailrls pt pos            ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)

 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);

     val t = get_obj g_form pt p

 	  val tac = get_obj g_tac pt p

 	  val rls = (assoc_rls o Tac.rls_of) tac

     val ctxt = get_ctxt pt pos

 val Seq _ = (*case*) rls (*of*);

 (*      val is = Generate.init_istate tac t  ..ERROR ,,>..>init_istate: "norm_Poly" has EmptyScr*)

 "~~~~~ fun init_istate, args:"; val ((Tac.Rewrite_Set rls), t) = (tac, t);

 val Celem.Seq {scr = Celem.Prog s,...} = (*case*) assoc_rls rls (*of*);

 "~~~~~ to detailrls return val:"; val is = (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))

 	      val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

 	      val pos' = ((lev_on o lev_dn) p, Ctree.Frm)

 	      val thy = Celem.assoc_thy "Isac"

 	      val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)

 	      val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')

 	      val newnds = children (get_nd pt'' p)

 	      val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*);

 "~~~~~ to detailstep return val:"; val xxx = ("detailrls", pt''', (p @ [length newnds], Res));

 "~~~~~ to interSteps return val:"; val ("detailrls", pt, lastpos) = xxx;

 show_pt pt;

 (*[

 (([], Frm), Simplify (b + a - b)),

 (([1], Frm), b + a - b),

 (([1,1], Frm), b + a - b),

 (([1,1], Res), b + a + -1 * b),

 (([1,2], Res), a + b + -1 * b),

 (([1,3], Res), a + 0 * b),

 (([1,4], Res), a),

 (([1], Res), a),

 (([], Res), a)]*)

 if existpt' ([1,4], Res) pt then ()

 else error  "scrtools.sml: auto-generated norm_Poly doesnt work";

 *} ML {*

 *} ML {*

 *} ML {*

 *} ML {*

 *} ML {*

 "~~~~~ fun xxx, args:"; val () = ();

 *}

   ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"