76 (* the parsing function returns a qualified name, we get back the base name *) |
76 (* the parsing function returns a qualified name, we get back the base name *) |
77 val atom_basename = Sign.base_name atom_name; |
77 val atom_basename = Sign.base_name atom_name; |
78 val goal = List.nth(prems_of thm, i-1); |
78 val goal = List.nth(prems_of thm, i-1); |
79 val ps = Logic.strip_params goal; |
79 val ps = Logic.strip_params goal; |
80 val Ts = rev (map snd ps); |
80 val Ts = rev (map snd ps); |
81 fun is_of_fs_name T = Type.of_sort (Sign.tsig_of thy) |
81 fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]); |
82 (T, Sign.intern_sort thy ["fs_"^atom_basename]); |
|
83 (* rebuild de bruijn indices *) |
82 (* rebuild de bruijn indices *) |
84 val bvs = map_index (Bound o fst) ps; |
83 val bvs = map_index (Bound o fst) ps; |
85 (* select variables of the right class *) |
84 (* select variables of the right class *) |
86 val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t))) |
85 val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t))) |
87 (term_frees goal @ bvs); |
86 (term_frees goal @ bvs); |