1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4  	  | ato (f$t')           n = ato f n^ato t' (n+1)
     1.5      in "\n-------------"^ato t 0^"\n" end;
     1.6  fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
     1.7 -    handle _ => raise error ("free2int: "^term2str t))
     1.8 -  | free2int t = raise error ("free2int: "^term2str t);
     1.9 +    handle _ => error ("free2int: "^term2str t))
    1.10 +  | free2int t = error ("free2int: "^term2str t);
    1.11  (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)
    1.12  
    1.13  
    1.14 @@ -56,12 +56,12 @@
    1.15  
    1.16  fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
    1.17      if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly 
    1.18 -    else raise error ("term2poly.1 "^term2str t1)
    1.19 +    else error ("term2poly.1 "^term2str t1)
    1.20    | mono (t as Const ("op *",_) $ t1 $ 
    1.21  	    (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
    1.22      if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] 
    1.23 -    else raise error ("term2poly.2 "^term2str t)
    1.24 -  | mono t _ _ = raise error ("term2poly.3 "^term2str t);
    1.25 +    else error ("term2poly.2 "^term2str t)
    1.26 +  | mono t _ _ = error ("term2poly.3 "^term2str t);
    1.27  
    1.28  fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = 
    1.29      let val l = mono t1 v g
    1.30 @@ -185,7 +185,7 @@
    1.31  "***************************************************************************";
    1.32  fun rewrite_set_' thy rls put_asm ruless ct =
    1.33      case ruless of
    1.34 -	Rrls _ => raise error "rewrite_set_' not for Rrls"
    1.35 +	Rrls _ => error "rewrite_set_' not for Rrls"
    1.36        | Rls _ =>
    1.37    let
    1.38      datatype switch = Appl | Noap;
    1.39 @@ -208,7 +208,7 @@
    1.40  		   rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 
    1.41  		   rls put_asm thm' ct;
    1.42  		 val _ = if pairopt <> NONE then () 
    1.43 -			 else raise error("rewrite_set_, rewrite_ \""^
    1.44 +			 else error("rewrite_set_, rewrite_ \""^
    1.45  			 (string_of_thmI thm')^"\" \""^
    1.46  			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
    1.47  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
    1.48 @@ -221,7 +221,7 @@
    1.49  *)
    1.50  fun rewrite_set_' thy rls put_asm ruless ct =
    1.51      case ruless of
    1.52 -	Rrls _ => raise error "rewrite_set_' not for Rrls"
    1.53 +	Rrls _ => error "rewrite_set_' not for Rrls"
    1.54        | Rls _ =>
    1.55    let
    1.56      datatype switch = Appl | Noap;
    1.57 @@ -244,7 +244,7 @@
    1.58  		   rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 
    1.59  		   rls put_asm thm' ct;
    1.60  		 val _ = if pairopt <> NONE then () 
    1.61 -			 else raise error("rewrite_set_, rewrite_ \""^
    1.62 +			 else error("rewrite_set_, rewrite_ \""^
    1.63  			 (string_of_thmI thm')^"\" \""^
    1.64  			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
    1.65  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);