# HG changeset patch
# User haftmann
# Date 1315893406 -7200
# Node ID 1886cddaf8a590df5923ed6e65901a40a21e3850
# Parent  7ef6505bde7f8f752715eac7ebeb5756da4debe8
tuned

diff -r 7ef6505bde7f -r 1886cddaf8a5 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Sep 14 10:08:52 2011 -0400
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Sep 13 07:56:46 2011 +0200
@@ -27,7 +27,7 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
-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 fresh_prod = @{thm fresh_prod};
 
diff -r 7ef6505bde7f -r 1886cddaf8a5 src/HOL/Nominal/nominal_inductive2.ML
--- 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};