199 fun next st = |
199 fun next st = |
200 Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} |
200 Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} |
201 (false, relift st, Thm.nprems_of st) gno state |
201 (false, relift st, Thm.nprems_of st) gno state |
202 in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; |
202 in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; |
203 |
203 |
204 fun print_vars_terms ctxt n thm = |
|
205 let |
|
206 fun typed s ty = " " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty; |
|
207 fun find_vars (Const (c, ty)) = |
|
208 if null (Term.add_tvarsT ty []) then I |
|
209 else insert (op =) (typed c ty) |
|
210 | find_vars (Var (xi, ty)) = |
|
211 insert (op =) (typed (Term.string_of_vname xi) ty) |
|
212 | find_vars (Free _) = I |
|
213 | find_vars (Bound _) = I |
|
214 | find_vars (Abs (_, _, t)) = find_vars t |
|
215 | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2; |
|
216 val prem = Logic.nth_prem (n, Thm.prop_of thm) |
|
217 val tms = find_vars prem [] |
|
218 in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; |
|
219 |
|
220 in |
204 in |
221 |
205 |
222 fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm |
206 fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm |
223 handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty) |
207 handle THM ("assume: variables", _, _) => Seq.empty |
224 |
208 |
225 end; |
209 end; |
226 |
210 |
227 |
211 |
228 (* generating identifiers -- often fresh *) |
212 (* generating identifiers -- often fresh *) |