equal
deleted
inserted
replaced
118 | map_to_alls f x = x; |
118 | map_to_alls f x = x; |
119 |
119 |
120 (* map a function f to each type variable in a term *) |
120 (* map a function f to each type variable in a term *) |
121 (* implicit arg: term *) |
121 (* implicit arg: term *) |
122 fun map_to_term_tvars f = |
122 fun map_to_term_tvars f = |
123 Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x); |
123 Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *) |
124 |
124 |
125 |
125 |
126 |
126 |
127 (* what if a param desn't occur in the concl? think about! Note: This |
127 (* what if a param desn't occur in the concl? think about! Note: This |
128 simply fixes meta level univ bound vars as Frees. At the end, we will |
128 simply fixes meta level univ bound vars as Frees. At the end, we will |