1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -95,15 +95,15 @@
     1.4  val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
     1.5  val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
     1.6             eval_kleiner "aaa" "bbb" t "ccc";
     1.7 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
     1.8 +"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
     1.9    ("aaa", "bbb", t, "ccc");
    1.10      (*if*) TermC.is_num b (*else*);
    1.11  
    1.12     	(*if*) identifier a < identifier b  (*else*);
    1.13  "~~~~~ fun identifier , args:"; val (t) = (a);
    1.14  (*+*)case a of
    1.15 -  Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
    1.16 -    (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
    1.17 +  Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
    1.18 +    (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.19  | _ => error "eval_kleiner CHANGED";                                                 (*isa*)
    1.20  ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.21