src/HOL/Nominal/nominal_inductive.ML

--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -28,7 +28,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 = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
 
 val fresh_prod = thm "fresh_prod";