don't pollute local theory with needless names

--- a/NEWS	Mon Nov 02 21:49:49 2015 +0100
+++ b/NEWS	Mon Nov 02 21:58:38 2015 +0100
@@ -400,7 +400,9 @@
   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     structure on the raw type to an abstract type defined using typedef.
   - Always generate "case_transfer" theorem.
-  - Allow discriminators and selectors with the same name as the type.
+  - Allow discriminators and selectors with the same name as the type
+    being defined.
+  - Avoid various internal name clashes (e.g., 'datatype f = f').
 
 * Transfer:
   - new methods for interactive debugging of 'transfer' and

--- a/src/HOL/BNF_Fixpoint_Base.thy	Mon Nov 02 21:49:49 2015 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Mon Nov 02 21:58:38 2015 +0100
@@ -14,9 +14,6 @@
 imports BNF_Composition Basic_BNFs
 begin
 
-lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
-  by standard simp_all
-
 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
   by standard simp_all
 

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 02 21:58:38 2015 +0100
@@ -105,14 +105,13 @@
   val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
   val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms
 
-  val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
-     typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
-     (term list
-      * (typ list list * typ list list list list * term list list * term list list list list) option
-      * (string * term list * term list list
-         * (((term list list * term list list * term list list list list * term list list list list)
-             * term list list list) * typ list)) option)
-     * Proof.context
+  val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list ->
+     typ list -> typ list -> typ list -> int list -> int list list -> term list ->
+     term list
+     * (typ list list * typ list list list list * term list list * term list list list list) option
+     * (string * term list * term list list
+        * (((term list list * term list list * term list list list list * term list list list list)
+            * term list list list) * typ list)) option
   val repair_nullary_single_ctr: typ list list -> typ list list
   val mk_corec_p_pred_types: typ list -> int list -> typ list list
   val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
@@ -1176,7 +1175,7 @@
   | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts
   | unzip_recT _ T = [T];
 
-fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
+fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts =
   let
     val Css = map2 replicate ns Cs;
     val x_Tssss =
@@ -1188,11 +1187,11 @@
     val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;
     val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css;
 
-    val ((fss, xssss), lthy) = lthy
+    val ((fss, xssss), _) = ctxt
       |> mk_Freess "f" f_Tss
       ||>> mk_Freessss "x" x_Tssss;
   in
-    ((f_Tss, x_Tssss, fss, xssss), lthy)
+    (f_Tss, x_Tssss, fss, xssss)
   end;
 
 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
@@ -1222,14 +1221,14 @@
    mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
      (binder_fun_types (fastype_of dtor_corec)));
 
-fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
+fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts =
   let
     val p_Tss = mk_corec_p_pred_types Cs ns;
 
     val (q_Tssss, g_Tsss, g_Tssss, corec_types) =
       mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
 
-    val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy
+    val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt
       |> yield_singleton (mk_Frees "x") dummyT
       ||>> mk_Frees "a" Cs
       ||>> mk_Freess "p" p_Tss
@@ -1238,7 +1237,7 @@
 
     val cpss = map2 (map o rapp) cs pss;
 
-    fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
+    fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd);
 
     fun build_dtor_corec_arg _ [] [cg] = cg
       | build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -1250,25 +1249,25 @@
     val cgssss = map2 (map o map o map o rapp) cs gssss;
     val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss;
   in
-    ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
+    (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types))
   end;
 
-fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
+fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 =
   let
-    val thy = Proof_Context.theory_of lthy;
+    val thy = Proof_Context.theory_of ctxt;
 
     val (xtor_co_rec_fun_Ts, xtor_co_recs) =
       mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
 
-    val ((recs_args_types, corecs_args_types), lthy') =
+    val (recs_args_types, corecs_args_types) =
       if fp = Least_FP then
-        mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
-        |>> (rpair NONE o SOME)
+        mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
+        |> (rpair NONE o SOME)
       else
-        mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
-        |>> (pair NONE o SOME);
+        mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
+        |> (pair NONE o SOME);
   in
-    ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
+    (xtor_co_recs, recs_args_types, corecs_args_types)
   end;
 
 fun mk_preds_getterss_join c cps absT abs cqgss =
@@ -2175,8 +2174,9 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
-      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+    val (xtor_co_recs, recs_args_types, corecs_args_types) =
+      mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
+    val lthy' = lthy;
 
     fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
         ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 02 21:58:38 2015 +0100
@@ -255,8 +255,8 @@
         val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
         val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
 
-        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
-          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+        val (xtor_co_recs, recs_args_types, corecs_args_types) =
+          mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
 
         fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;