1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -280,8 +280,8 @@
     1.4  
     1.5  case (op_, t) of
     1.6    ("Transcendental.powr",
     1.7 -    Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
     1.8 -      (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()
     1.9 +    Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.10 +      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.11  | _ => error "3 \<up> 2 CHANGED";
    1.12    val SOME (id, t') = eval_binop thmid op_ t thy;
    1.13  (*** calc: operator = pow not defined*)
    1.14 @@ -303,8 +303,8 @@
    1.15  val (t1, t2) = (@{term 3}, @{term "2::real"});
    1.16  
    1.17  "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
    1.18 -    val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;
    1.19 -    val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;
    1.20 +    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
    1.21 +    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
    1.22      val (T, _) = HOLogic.dest_number t1
    1.23      val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
    1.24      val result =