src/HOL/Nominal/nominal_datatype.ML

--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 16:25:27 2009 +0100
@@ -567,13 +567,16 @@
     val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
-        Inductive.add_inductive_global (serial ())
+      thy3
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
-          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
+          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+      ||> Sign.restore_naming thy3;
 
     (**** Prove that representing set is closed under permutation ****)
 
@@ -1508,15 +1511,17 @@
           ([], [], [], [], 0);
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
-      thy10 |>
-        Inductive.add_inductive_global (serial ())
+      thy10
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
-      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
+          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+      ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
+      ||> Sign.restore_naming thy10;
 
     (** equivariance **)