1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Mon Aug 23 12:33:10 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Mon Aug 23 14:24:06 2021 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4   case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
     1.5  	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
     1.6  *)
     1.7 -if f2str f = "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" then ()
     1.8 +if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
     1.9  else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
    1.10  
    1.11  
    1.12 @@ -212,6 +212,7 @@
    1.13  "----------- rls make_polynomial_in ------------------------------";
    1.14  "----------- rls make_polynomial_in ------------------------------";
    1.15  "----------- rls make_polynomial_in ------------------------------";
    1.16 +val thy = @{theory};
    1.17  (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
    1.18  (*WN.19.3.03 ---v-*)
    1.19  (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
    1.20 @@ -283,18 +284,18 @@
    1.21  
    1.22  (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
    1.23  t |> UnparseC.term; t |> TermC.atomty;
    1.24 -val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
    1.25 +val thm = @{thm d2_prescind1};
    1.26  thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
    1.27  val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
    1.28  
    1.29  (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
    1.30                                                                          --> x = 0 | -6 + 5 * x = 0*)
    1.31  t' |> UnparseC.term; t' |> TermC.atomty;
    1.32 -val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
    1.33 +val thm = @{thm d2_reduce_equation1};
    1.34  thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
    1.35  val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
    1.36  (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    1.37     instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
    1.38  *)
    1.39 -if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
    1.40 +if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
    1.41  else error "rls d2_polyeq_bdv_only_simplify broken";