equal
deleted
inserted
replaced
1225 fun close_frees t = |
1225 fun close_frees t = |
1226 let |
1226 let |
1227 val rev_frees = |
1227 val rev_frees = |
1228 Term.fold_aterms (fn Free (x, T) => |
1228 Term.fold_aterms (fn Free (x, T) => |
1229 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; |
1229 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; |
1230 in Term.list_all_free (rev_frees, t) end; |
1230 in Term.list_all_free (rev rev_frees, t) end; |
1231 |
1231 |
1232 fun no_binds [] = [] |
1232 fun no_binds [] = [] |
1233 | no_binds _ = error "Illegal term bindings in locale element"; |
1233 | no_binds _ = error "Illegal term bindings in locale element"; |
1234 in |
1234 in |
1235 (case elem of |
1235 (case elem of |