src/HOL/Tools/inductive.ML
changeset 40316 665862241968
parent 39248 4a3747517552
child 40902 7c652e4a924a
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Nov 03 10:51:40 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Nov 03 11:06:22 2010 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  fun arg_types_of k c = drop k (binder_types (fastype_of c));
     1.6  
     1.7 -fun find_arg T x [] = sys_error "find_arg"
     1.8 +fun find_arg T x [] = raise Fail "find_arg"
     1.9    | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
    1.10        apsnd (cons p) (find_arg T x ps)
    1.11    | find_arg T x ((p as (U, (NONE, y))) :: ps) =