src/HOL/Tools/inductive_package.ML
changeset 23577 c5b93c69afd3
parent 22997 d4f3b015b50b
child 23762 24eef53a9ad3
--- a/src/HOL/Tools/inductive_package.ML	Thu Jul 05 00:06:13 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 05 00:06:14 2007 +0200
@@ -194,7 +194,7 @@
   | 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 =