140 fun index_elims c = |
140 fun index_elims c = |
141 let fun topc(_,thm) = elim_const thm = Some(c); |
141 let fun topc(_,thm) = elim_const thm = Some(c); |
142 val named_thms = thms_containing [c] |
142 val named_thms = thms_containing [c] |
143 in filter topc named_thms end; |
143 in filter topc named_thms end; |
144 |
144 |
145 (*assume that parameters have unique names*) |
145 (*assume that parameters have unique names; reverse them for substitution*) |
146 fun goal_params i = |
146 fun goal_params i = |
147 let val gi = getgoal i |
147 let val gi = getgoal i |
148 val frees = map Free (Logic.strip_params gi) |
148 val rfrees = rev(map Free (Logic.strip_params gi)) |
149 in (gi,frees) end; |
149 in (gi,rfrees) end; |
150 |
150 |
151 fun concl_of_goal i = |
151 fun concl_of_goal i = |
152 let val (gi,frees) = goal_params i |
152 let val (gi,rfrees) = goal_params i |
153 val B = Logic.strip_assums_concl gi |
153 val B = Logic.strip_assums_concl gi |
154 in subst_bounds(frees,B) end; |
154 in subst_bounds(rfrees,B) end; |
155 |
155 |
156 fun prems_of_goal i = |
156 fun prems_of_goal i = |
157 let val (gi,frees) = goal_params i |
157 let val (gi,rfrees) = goal_params i |
158 val As = Logic.strip_assums_hyp gi |
158 val As = Logic.strip_assums_hyp gi |
159 in map (fn A => subst_bounds(frees,A)) As end; |
159 in map (fn A => subst_bounds(rfrees,A)) As end; |
160 |
160 |
161 (*returns all those named_thms whose subterm extracted by extract can be |
161 (*returns all those named_thms whose subterm extracted by extract can be |
162 instantiated to obj; the list is sorted according to the number of premises |
162 instantiated to obj; the list is sorted according to the number of premises |
163 and the size of the required substitution.*) |
163 and the size of the required substitution.*) |
164 fun select_match(obj, signobj, named_thms, extract) = |
164 fun select_match(obj, signobj, named_thms, extract) = |