diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:27 2009 +0200
@@ -103,8 +103,8 @@
           NONE => error "index_of : type not found in environements!"
         | SOME (tbs,tats) =>
           let
-            val i = find_index_eq t tats
-            val j = find_index_eq t tbs
+            val i = find_index (fn t' => t' = t) tats
+            val j = find_index (fn t' => t' = t) tbs
           in (if j = ~1 then
               if i = ~1
               then (length tbs + length tats,