equal
deleted
inserted
replaced
1047 let |
1047 let |
1048 val thm = Thm.close_derivation raw_thm; |
1048 val thm = Thm.close_derivation raw_thm; |
1049 val c = const_eqn thy thm; |
1049 val c = const_eqn thy thm; |
1050 fun update_subsume thy (thm, proper) eqns = |
1050 fun update_subsume thy (thm, proper) eqns = |
1051 let |
1051 let |
1052 val args_of = snd o strip_comb o map_types Type.strip_sorts |
1052 val args_of = dropwhile is_Var o rev o snd o strip_comb |
1053 o fst o Logic.dest_equals o Thm.plain_prop_of; |
1053 o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; |
1054 val args = args_of thm; |
1054 val args = args_of thm; |
1055 val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); |
1055 val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); |
1056 fun matches_args args' = length args <= length args' andalso |
1056 fun matches_args args' = length args <= length args' andalso |
1057 Pattern.matchess thy (args, (map incr_idx o take (length args)) args'); |
1057 Pattern.matchess thy (args, (map incr_idx o take (length args)) args'); |
1058 fun drop (thm', proper') = if (proper orelse not proper') |
1058 fun drop (thm', proper') = if (proper orelse not proper') |