src/HOL/Tools/inductive_package.ML

 
 fun find_arg T x [] = sys_error "find_arg"
   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
       apsnd (cons p) (find_arg T x ps)
   | find_arg T x ((p as (U, (NONE, y))) :: ps) =
-      if T = U then (y, (U, (SOME x, y)) :: ps)
+      if (T: typ) = U then (y, (U, (SOME x, y)) :: ps)
       else apsnd (cons p) (find_arg T x ps);
 
 fun make_args Ts xs =
   map (fn (T, (NONE, ())) => Const ("arbitrary", T) | (_, (SOME t, ())) => t)
     (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));