1.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:25 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:27 2009 +0200
     1.3 @@ -103,8 +103,8 @@
     1.4            NONE => error "index_of : type not found in environements!"
     1.5          | SOME (tbs,tats) =>
     1.6            let
     1.7 -            val i = find_index_eq t tats
     1.8 -            val j = find_index_eq t tbs
     1.9 +            val i = find_index (fn t' => t' = t) tats
    1.10 +            val j = find_index (fn t' => t' = t) tbs
    1.11            in (if j = ~1 then
    1.12                if i = ~1
    1.13                then (length tbs + length tats,