src/HOL/Tools/Old_Datatype/old_datatype.ML
changeset 59859 f9d1442c70f3
parent 59621 291934bac95e
child 59880 30687c3f2b10
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Mar 30 22:34:59 2015 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 00:11:54 2015 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     1.6        thy1
     1.7 -      |> Sign.map_naming Name_Space.conceal
     1.8 +      |> Sign.map_naming Name_Space.concealed
     1.9        |> Inductive.add_inductive_global
    1.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    1.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}