src/HOL/Nominal/nominal_inductive.ML
changeset 33049 c38f02fdf35d
parent 33040 cffdb7b28498
child 33368 b1cf34f1855c
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 10:15:31 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 12:09:37 2009 +0200
     1.3 @@ -28,7 +28,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) (ps, Term.add_frees t []);
     1.8 +fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     1.9  
    1.10  val fresh_prod = thm "fresh_prod";
    1.11