src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33171 292970b42770
parent 33063 4d462963a7db
child 33173 b8ca12f6681a
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:19:41 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:21:34 2009 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4          (descr' ~~ recTs ~~ rec_sets') ([], 0);
     1.5  
     1.6      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     1.7 -        Inductive.add_inductive_global (serial_string ())
     1.8 +        Inductive.add_inductive_global (serial ())
     1.9            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.10              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    1.11              skip_mono = true, fork_mono = false}