--- a/src/Pure/Isar/code.ML Thu May 14 09:16:34 2009 +0200
+++ b/src/Pure/Isar/code.ML Thu May 14 09:16:36 2009 +0200
@@ -116,7 +116,8 @@
fun add_drop_redundant thy (thm, proper) thms =
let
- val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
+ val args_of = snd o strip_comb o map_types Type.strip_sorts
+ o fst o Logic.dest_equals o Thm.plain_prop_of;
val args = args_of thm;
val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
fun matches_args args' = length args <= length args' andalso