changeset 31986 | a68f88d264f7 |
parent 31810 | a6b800855cdd |
child 32032 | a6a6e8031c14 |
--- 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,