tuned
authorhaftmann
Tue Sep 13 07:56:46 2011 +0200 (2011-09-13)
changeset 449291886cddaf8a5
parent 44928 7ef6505bde7f
child 44930 afcbf23508af
tuned
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Sep 14 10:08:52 2011 -0400
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Sep 13 07:56:46 2011 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
     1.5    (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
     1.6  
     1.7 -fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     1.8 +fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
     1.9  
    1.10  val fresh_prod = @{thm fresh_prod};
    1.11  
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Sep 14 10:08:52 2011 -0400
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Sep 13 07:56:46 2011 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4      [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
     2.5       @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
     2.6  
     2.7 -fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     2.8 +fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
     2.9  
    2.10  val perm_bool = mk_meta_eq @{thm perm_bool_def};
    2.11  val perm_boolI = @{thm perm_boolI};