author | wenzelm |
Mon, 17 Mar 2008 18:36:04 +0100 | |
changeset 26299 | 2f387f5c0f52 |
parent 26298 | 53e382ccf71f |
child 26300 | 03def556e26e |
--- a/src/Pure/Isar/locale.ML Mon Mar 17 16:47:45 2008 +0100 +++ b/src/Pure/Isar/locale.ML Mon Mar 17 18:36:04 2008 +0100 @@ -1227,7 +1227,7 @@ val rev_frees = Term.fold_aterms (fn Free (x, T) => if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; - in Term.list_all_free (rev_frees, t) end; + in Term.list_all_free (rev rev_frees, t) end; fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in locale element";