src/HOL/Tools/datatype_realizer.ML
changeset 23577 c5b93c69afd3
parent 22691 290454649b8c
child 23590 ad95084a5c63
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 00:06:13 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 00:06:14 2007 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4   
     1.5      fun mk_proj j [] t = t
     1.6        | mk_proj j (i :: is) t = if null is then t else
     1.7 -          if j = i then HOLogic.mk_fst t
     1.8 +          if (j: int) = i then HOLogic.mk_fst t
     1.9            else mk_proj j is (HOLogic.mk_snd t);
    1.10  
    1.11      val tnames = DatatypeProp.make_tnames recTs;