src/HOL/Tools/inductive_realizer.ML
changeset 33726 0878aecbf119
parent 33671 4b0f2599ed48
child 33955 fff6f11b1f09
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Nov 17 14:51:32 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Nov 17 14:51:57 2009 +0100
     1.3 @@ -350,7 +350,7 @@
     1.4      (** realizability predicate **)
     1.5  
     1.6      val (ind_info, thy3') = thy2 |>
     1.7 -      Inductive.add_inductive_global (serial ())
     1.8 +      Inductive.add_inductive_global
     1.9          {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    1.10            no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.11          rlzpreds rlzparams (map (fn (rintr, intr) =>