Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_realizer.ML
changeset 49170 03bee3a6a1b7
parent 47060 e2741ec9ae36
child 51717 9e7d1c139569 
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 19:51:00 2012 +0200
@@ -355,7 +355,7 @@
     val (ind_info, thy3') = thy2 |>
       Inductive.add_inductive_global
         {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
-          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+          no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
isabelle