equal
deleted
inserted
replaced
114 val thy_ref = Theory.check_thy thy; |
114 val thy_ref = Theory.check_thy thy; |
115 in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; |
115 in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; |
116 |
116 |
117 fun add_drop_redundant thy (thm, proper) thms = |
117 fun add_drop_redundant thy (thm, proper) thms = |
118 let |
118 let |
119 val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
119 val args_of = snd o strip_comb o map_types Type.strip_sorts |
|
120 o fst o Logic.dest_equals o Thm.plain_prop_of; |
120 val args = args_of thm; |
121 val args = args_of thm; |
121 val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); |
122 val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); |
122 fun matches_args args' = length args <= length args' andalso |
123 fun matches_args args' = length args <= length args' andalso |
123 Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); |
124 Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); |
124 fun drop (thm', proper') = if (proper orelse not proper') |
125 fun drop (thm', proper') = if (proper orelse not proper') |