src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
changeset 31723 f5cafe803b55
parent 31668 a616e56a5ec8
child 31737 b3f63611784e
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -155,7 +155,7 @@
     1.4          (([], 0), descr' ~~ recTs ~~ rec_sets');
     1.5  
     1.6      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     1.7 -        InductivePackage.add_inductive_global (serial_string ())
     1.8 +        Inductive.add_inductive_global (serial_string ())
     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}