src/HOL/Tools/Old_Datatype/old_datatype.ML

--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -172,7 +172,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       thy1
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}