| changeset 44929 | 1886cddaf8a5 |
| parent 44868 | 92be5b32ca71 |
| child 46218 | ecf6375e2abb |
--- 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};