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