src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -355,9 +355,8 @@
     1.4                thy
     1.5                |> Sign.map_naming Name_Space.conceal
     1.6                |> Inductive.add_inductive_global (serial ())
     1.7 -                {quiet_mode = false, verbose = false, kind = "",
     1.8 -                  alt_name = Binding.empty, coind = false, no_elim = false,
     1.9 -                  no_ind = false, skip_mono = false, fork_mono = false}
    1.10 +                {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    1.11 +                  no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.12                  (map (fn (s, T) =>
    1.13                    ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
    1.14                  pnames