diff -r 716f399db0a5 -r d4ebe139100d test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Sep 16 12:23:57 2021 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Sep 16 17:23:54 2021 +0200
@@ -243,9 +243,9 @@
   | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
   | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
 
-fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $ 
+fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $ 
       Free (var, _) $ Free (pot, _)) =
-    (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
+    (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
     case x of                                                          (*WN*)
 	    (Free (xstr, _)) => 
 		    if xstr = var