# HG changeset patch
# User blanchet
# Date 1388756293 -3600
# Node ID a5a2598f0651ed74c4f289ace3566a861450aa44
# Parent  28b621fce2f9d15feefa8139191305b45b44a082
proper name generation to avoid clash with 'P' in user specification

diff -r 28b621fce2f9 -r a5a2598f0651 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 14:14:16 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 14:38:13 2014 +0100
@@ -979,6 +979,9 @@
           |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I);
         val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn;
 
+        val ps =
+          Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
+
         val exhaust_thmss =
           map2 (fn false => K []
               | true => fn disc_eqns as {fun_args, ...} :: _ =>
@@ -989,7 +992,7 @@
                   [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)]
                 end)
             de_facto_exhaustives disc_eqnss
-          |> list_all_fun_args [("P", HOLogic.boolT)]
+          |> list_all_fun_args ps
           |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
               | [nchotomy_thm] => fn [goal] =>
                 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)