--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Sep 14 10:08:52 2011 -0400
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Sep 13 07:56:46 2011 +0200
@@ -33,7 +33,7 @@
[@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
@{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
-fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
+fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
val perm_bool = mk_meta_eq @{thm perm_bool_def};
val perm_boolI = @{thm perm_boolI};