# HG changeset patch
# User haftmann
# Date 1284016273 -7200
# Node ID 4a37475175529b1a683be1e136d28ffc1ffcc880
# Parent  3a15ee47c6106f48a2dd883ff7604ba9dfc0f2f9
only conceal primitive definition theorems, not predicate names

diff -r 3a15ee47c610 -r 4a3747517552 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 08 19:23:23 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Sep 09 09:11:13 2010 +0200
@@ -789,14 +789,12 @@
             val xs = map Free (Variable.variant_frees lthy intr_ts
               (mk_names "x" (length Ts) ~~ Ts))
           in
-            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
+            (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
               (list_comb (rec_const, params @ make_bool_args' bs i @
                 make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
-      |> Local_Theory.conceal
-      |> fold_map Local_Theory.define specs
-      ||> Local_Theory.restore_naming lthy';
+      |> fold_map Local_Theory.define specs;
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';