src/HOL/Tools/inductive_set.ML
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33670 02b7738aef6a
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4    map (fn (x, ps) =>
     1.5      let
     1.6        val U = HOLogic.dest_setT (fastype_of x);
     1.7 -      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
     1.8 +      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     1.9      in
    1.10        (cterm_of thy x,
    1.11         cterm_of thy (HOLogic.Collect_const U $
    1.12 @@ -405,7 +405,7 @@
    1.13  (**** definition of inductive sets ****)
    1.14  
    1.15  fun add_ind_set_def
    1.16 -    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    1.17 +    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    1.18      cs intros monos params cnames_syn lthy =
    1.19    let
    1.20      val thy = ProofContext.theory_of lthy;
    1.21 @@ -477,7 +477,7 @@
    1.22      val monos' = map (to_pred [] (Context.Proof lthy)) monos;
    1.23      val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
    1.24        Inductive.add_ind_def
    1.25 -        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
    1.26 +        {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
    1.27            coind = coind, no_elim = no_elim, no_ind = no_ind,
    1.28            skip_mono = skip_mono, fork_mono = fork_mono}
    1.29          cs' intros' monos' params1 cnames_syn' lthy;
    1.30 @@ -505,7 +505,7 @@
    1.31              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    1.32                [def, mem_Collect_eq, split_conv]) 1))
    1.33          in
    1.34 -          lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.35 +          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.36              [Attrib.internal (K pred_set_conv_att)]),
    1.37                [conv_thm]) |> snd
    1.38          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
    1.39 @@ -519,7 +519,7 @@
    1.40      val (intr_names, intr_atts) = split_list (map fst intros);
    1.41      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
    1.42      val (intrs', elims', induct, lthy4) =
    1.43 -      Inductive.declare_rules kind rec_name coind no_ind cnames
    1.44 +      Inductive.declare_rules rec_name coind no_ind cnames
    1.45          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    1.46          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    1.47             map fst (fst (Rule_Cases.get th)))) elims)