--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Tue Mar 31 00:11:54 2015 +0200
@@ -146,7 +146,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
- |> Sign.map_naming Name_Space.conceal
+ |> Sign.map_naming Name_Space.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
coind = false, no_elim = false, no_ind = true, skip_mono = true}