diff -r 3e9b709fc755 -r d74e7e33db35 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Aug 04 17:34:47 2021 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 05 18:05:28 2021 +0200
@@ -35,19 +35,16 @@
 "----------- fun identifier --------------------------------------------------------------------";
 "----------- fun identifier --------------------------------------------------------------------";
 "----------- fun identifier --------------------------------------------------------------------";
-(*+*)identifier (TermC.str2term "12 ::real") = "|||||||||||||";
-(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
 if identifier (TermC.str2term "12 ::real") = "12"     then () else error "identifier 1";
-( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
+if identifier (TermC.str2term
+  "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
+                                                      then () else error "identifier 1a";
 
 if identifier (TermC.str2term "a ::real") = "a"       then () else error "identifier 2";
 if identifier (TermC.str2term "3 * a ::real") = "a"   then () else error "identifier 3";
 
-(*+*)identifier (TermC.str2term "a \<up> 2 ::real") = "|||||||||||||";(*TOODOO <-- START HERE*)
-(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
 if identifier (TermC.str2term "a \<up> 2 ::real") = "a"   then () else error "identifier 4";
 if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
-( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
 if identifier (TermC.str2term "a * b ::real") = "b"   then () else error "identifier 5b";
 
 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
@@ -67,8 +64,6 @@
 TermC.str2term "aaa";
 TermC.str2term "222 * aaa";
 
-(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
-(*TOODOO eval_kleiner *)
 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
     SOME ("123 kleiner 32 = False", _) => ()
   | _ => error "polyminus.sml: 12 kleiner 9 = False";
@@ -95,7 +90,7 @@
 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
            eval_kleiner "aaa" "bbb" t "ccc";
-"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
+"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
   ("aaa", "bbb", t, "ccc");
     (*if*) TermC.is_num b (*else*);
 
@@ -105,7 +100,6 @@
   Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
     (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
 | _ => error "eval_kleiner CHANGED";                                                 (*isa*)
-( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
 
 
 "----------- fun ist_monom ---------------------------------------------------------------------";
@@ -372,20 +366,11 @@
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
-   f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";      (*isa == isa2*)
-val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
-   val                 Check_Postcond ["plus_minus", "polynom", "vereinfachen"] = nxt;
-nxt;
-(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
-   val                              (*TOODOO*) Rewrite_Set "ordne_alphabetisch" = nxt;
-   f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";    (*isa2*)
-val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
-   f2str f = "3 + - 2 * e + 2 * f + 2 * g";                                  (*isa2*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
-   f2str f = "3 - 2 * e + 2 * f + 2 * g";                                    (*isa2*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
-   f2str f = "3 - 2 * e + 2 * f + 2 * g";                                    (*isa2*)
-if f2str f = "3 - 2 * e + 2 * f + 2 * g"                                     (*isa2*)
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+if f2str f = "3 - 2 * e + 2 * f + 2 * g" 
 then case nxt of End_Proof' => () | _ =>  error "me simplification.for_polynomials.with_minus 1"
 else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
 
@@ -417,7 +402,6 @@
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
 then () else error "polyminus.sml: Vereinfache 140 d)";
-( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
 
 "======= 139 c ---";
 reset_states ();