1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -1155,7 +1155,7 @@
     1.4    | pr_ord GREATER = "GREATER";
     1.5  
     1.6  fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
     1.7 -  | dest_hd' x (t as Free (a, T)) =
     1.8 +  | dest_hd' x (t as Free (a, T)) =          (*TODOO handle this as numeral, too? see EqSystem.thy*)
     1.9      if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)
    1.10      else (((a, 0), T), 1)
    1.11    | dest_hd' _ (Var v) = (v, 2)
    1.12 @@ -1163,18 +1163,17 @@
    1.13    | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
    1.14    | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
    1.15  
    1.16 -fun size_of_term' x (Const ("Transcendental.powr",_) $ Free (var,_) $ Free (pot,_)) =
    1.17 +fun size_of_term' x (Const ("Transcendental.powr",_) $
    1.18 +      Free (var, _) $ Const ("Num.numeral_class.numeral", _) $ pot) =
    1.19      (case x of                                                          (*WN*)
    1.20 -	    (Free (xstr,_)) => 
    1.21 -		(if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3)
    1.22 -	  | _ => raise ERROR ("size_of_term' called with subst = "^
    1.23 -			      (UnparseC.term x)))
    1.24 -  | size_of_term' x (Free (subst,_)) =
    1.25 +	    (Free (xstr, _)) => 
    1.26 +		    (if xstr = var then 1000 * (HOLogic.dest_numeral pot) else 3)
    1.27 +	  | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
    1.28 +  | size_of_term' x (Free (subst, _)) =
    1.29      (case x of
    1.30 -	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
    1.31 -	  | _ => raise ERROR ("size_of_term' called with subst = "^
    1.32 -			  (UnparseC.term x)))
    1.33 -  | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
    1.34 +	    (Free (xstr, _)) => (if xstr = subst then 1000 else 1)
    1.35 +	  | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
    1.36 +  | size_of_term' x (Abs (_, _, body)) = 1 + size_of_term' x body
    1.37    | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t
    1.38    | size_of_term' _ _ = 1;
    1.39