diff -r fa9e563f6bcf -r f8cd46077224 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri May 24 17:04:04 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 17:14:06 2013 +0200
@@ -137,7 +137,7 @@
 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
 fun split_type (T,0,Ts)                    = (Ts,T)
   | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
-  | split_type _                           = error("split_type");
+  | split_type _                           = raise Fail "split_type";
 
 fun type_of_G env (T, n, is) =
   let
@@ -204,7 +204,7 @@
     let fun mk([],[],_)        = []
           | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
                                         else mk(is,js,k-1)
-          | mk _               = error"mk_ff_list"
+          | mk _               = raise Fail "mk_ff_list"
     in mk(is,js,length is-1) end;
 
 fun flexflex1(env,binders,F,Fty,is,js) =