src/HOL/Tools/inductive.ML
changeset 31986 a68f88d264f7
parent 31902 862ae16a799d
child 32035 8e77b6a250d5
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 10 07:59:25 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 10 07:59:27 2009 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4      val k = length params;
     1.5      val (c, ts) = strip_comb t;
     1.6      val (xs, ys) = chop k ts;
     1.7 -    val i = find_index_eq c cs;
     1.8 +    val i = find_index (fn c' => c' = c) cs;
     1.9    in
    1.10      if xs = params andalso i >= 0 then
    1.11        SOME (c, i, ys, chop (length ys)