1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -1316,12 +1316,12 @@
     1.4      (case x of                                                          (*WN*)
     1.5  	    (Free (xstr,_)) => 
     1.6  		(if xstr = var then 1000*(the (int_of_str pot)) else 3)
     1.7 -	  | _ => raise error ("size_of_term' called with subst = "^
     1.8 +	  | _ => error ("size_of_term' called with subst = "^
     1.9  			      (term2str x)))
    1.10    | size_of_term' x (Free (subst,_)) =
    1.11      (case x of
    1.12  	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
    1.13 -	  | _ => raise error ("size_of_term' called with subst = "^
    1.14 +	  | _ => error ("size_of_term' called with subst = "^
    1.15  			  (term2str x)))
    1.16    | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
    1.17    | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t
    1.18 @@ -1369,7 +1369,7 @@
    1.19      in
    1.20  	case subst of
    1.21  	    (_,x)::_ => (term_ord' x pr thy tu = LESS)
    1.22 -	  | _ => raise error ("ord_make_polynomial_in called with subst = "^
    1.23 +	  | _ => error ("ord_make_polynomial_in called with subst = "^
    1.24  			  (subst2str subst))
    1.25      end;
    1.26  end;(*local*)