1.1 --- a/src/Tools/isac/Interpret/derive.sml	Tue Aug 16 12:21:21 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Tue Aug 16 14:47:05 2022 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  
     1.5  fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
     1.6  
     1.7 -(* fo = ifo excluded already in inform *)
     1.8 +(* case fo = ifo excluded already in inform *)
     1.9  fun steps ctxt rew_ord erls rules fo ifo =
    1.10    let 
    1.11      fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty

     2.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue Aug 16 12:21:21 2022 +0200
     2.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue Aug 16 14:47:05 2022 +0200
     2.3 @@ -350,30 +350,6 @@
     2.4  "~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1  \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
     2.5    (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
     2.6  
     2.7 -(*/----- original before child of 7e314dd233fd -------------------------------------------------\* )
     2.8 -    val (Program.Tac prog_tac, form_arg) = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
     2.9 -      val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
    2.10 -      val ORundef = (*case*) or (*of*);
    2.11 -  val Applicable.No "norm_equation not applicable" =    
    2.12 -      (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (pt, p) (*of*);
    2.13 -
    2.14 -   (Term_Val1 act_arg) (* return value *);
    2.15 -
    2.16 -val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
    2.17 -   t, (res, asm)) = m;
    2.18 -
    2.19 -if pstate2str ist =
    2.20 -  "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], empty, SOME t_t, \n" ^
    2.21 -  "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, true, false)"
    2.22 -andalso
    2.23 -  UnparseC.term t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
    2.24 -andalso
    2.25 -  UnparseC.term res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
    2.26 -andalso
    2.27 -  UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
    2.28 -then () else error "locate_input_tactic Helpless, but applicable CHANGED";
    2.29 -( *\----- original before child of 7e314dd233fd -------------------------------------------------/*)
    2.30 -
    2.31  val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
    2.32  val ([3], Res) = p;
    2.33  

     3.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Tue Aug 16 12:21:21 2022 +0200
     3.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Tue Aug 16 14:47:05 2022 +0200
     3.3 @@ -318,7 +318,7 @@
     3.4  	  val {nrls, ...} = MethodC.from_store (get_obj g_metID pt (par_pblobj pt p))
     3.5  	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
     3.6  	  (*val (found, der) = *)Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
     3.7 -"~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
     3.8 +"~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
     3.9    (rew_ord, erls, rules, fo, ifo);
    3.10      fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
    3.11        | derivat dt = (#1 o #3 o last_elem) dt