# HG changeset patch
# User haftmann
# Date 1417013179 -3600
# Node ID 5f060de2dfd651fd06290f1e2b1da0be448afc81
# Parent  97b089c4aa4610770f5685fba21099e709d4e144
do not conceal inductive predicate names properly, following 4a3747517552

diff -r 97b089c4aa46 -r 5f060de2dfd6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 26 15:46:17 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 26 15:46:19 2014 +0100
@@ -827,14 +827,15 @@
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
+    val is_auxiliary = length cs >= 2; 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> Local_Theory.conceal
+      |> is_auxiliary ? Local_Theory.conceal
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
+         ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> Local_Theory.restore_naming lthy;
+      ||> is_auxiliary ? Local_Theory.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
         (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));