src/HOL/Tools/inductive_realizer.ML
changeset 24816 2d0fa8f31804
parent 24746 6d42be359d57
child 24926 bcb6b098df11
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:26 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:28 2007 +0200
     1.3 @@ -350,7 +350,8 @@
     1.4      (** realizability predicate **)
     1.5  
     1.6      val (ind_info, thy3') = thy2 |>
     1.7 -      InductivePackage.add_inductive_global false "" false false false
     1.8 +      InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     1.9 +          alt_name = "", coind = false, no_elim = false, no_ind = false}
    1.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.11            ((Sign.base_name (name_of_thm intr), []),
    1.12             subst_atomic rlzpreds' (Logic.unvarify rintr)))