fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =

 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =

     (case x of                                                          (*WN*)

     (case x of                                                          (*WN*)

 	    (Free (xstr,_)) => 

 	    (Free (xstr,_)) => 

 		(if xstr = var then 1000*(the (int_of_str pot)) else 3)

 		(if xstr = var then 1000*(the (int_of_str pot)) else 3)

 			      (term2str x)))

 			      (term2str x)))

   | size_of_term' x (Free (subst,_)) =

   | size_of_term' x (Free (subst,_)) =

     (case x of

     (case x of

 	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)

 	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)

 			  (term2str x)))

 			  (term2str x)))

   | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body

   | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body

   | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t

   | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t

   | size_of_term' x _ = 1;

   | size_of_term' x _ = 1;

     let

     let

 	(* val _=tracing("*** subs variable is: "^(subst2str subst)); *)

 	(* val _=tracing("*** subs variable is: "^(subst2str subst)); *)

     in

     in

 	case subst of

 	case subst of

 	    (_,x)::_ => (term_ord' x pr thy tu = LESS)

 	    (_,x)::_ => (term_ord' x pr thy tu = LESS)

 			  (subst2str subst))

 			  (subst2str subst))

     end;

     end;

 end;(*local*)

 end;(*local*)

 *}

 *}