diff -r 7701598a2182 -r dcb37736d573 test/Tools/isac/ProgLang/evaluate.sml
--- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Jul 19 15:34:54 2021 +0200
+++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Jul 19 17:29:35 2021 +0200
@@ -280,8 +280,8 @@
 
 case (op_, t) of
   ("Transcendental.powr",
-    Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
-      (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()
+    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>, _))) $
+      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
 | _ => error "3 \<up> 2 CHANGED";
   val SOME (id, t') = eval_binop thmid op_ t thy;
 (*** calc: operator = pow not defined*)
@@ -303,8 +303,8 @@
 val (t1, t2) = (@{term 3}, @{term "2::real"});
 
 "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
-    val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;
-    val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;
+    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
+    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
     val (T, _) = HOLogic.dest_number t1
     val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
     val result =