--- a/src/HOL/Tools/inductive_set.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 19:57:46 2009 +0100
@@ -224,7 +224,7 @@
map (fn (x, ps) =>
let
val U = HOLogic.dest_setT (fastype_of x);
- val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
+ val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
in
(cterm_of thy x,
cterm_of thy (HOLogic.Collect_const U $
@@ -405,7 +405,7 @@
(**** definition of inductive sets ****)
fun add_ind_set_def
- {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+ {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -477,7 +477,7 @@
val monos' = map (to_pred [] (Context.Proof lthy)) monos;
val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
Inductive.add_ind_def
- {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
+ {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind,
skip_mono = skip_mono, fork_mono = fork_mono}
cs' intros' monos' params1 cnames_syn' lthy;
@@ -505,7 +505,7 @@
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
in
- lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
+ lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
[conv_thm]) |> snd
end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
@@ -519,7 +519,7 @@
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
val (intrs', elims', induct, lthy4) =
- Inductive.declare_rules kind rec_name coind no_ind cnames
+ Inductive.declare_rules rec_name coind no_ind cnames
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
map fst (fst (Rule_Cases.get th)))) elims)