--- a/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 19:57:46 2009 +0100
@@ -569,9 +569,8 @@
thy3
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = "",
- alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true, fork_mono = false}
+ {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
+ coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
[] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
@@ -1513,9 +1512,8 @@
thy10
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = "",
- alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
- skip_mono = true, fork_mono = false}
+ {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
+ coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 19:57:46 2009 +0100
@@ -156,9 +156,8 @@
thy0
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = "",
- alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
- skip_mono = true, fork_mono = false}
+ {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
+ coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 19:57:46 2009 +0100
@@ -175,9 +175,8 @@
thy1
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = "",
- alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true, fork_mono = false}
+ {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
+ coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (Attrib.empty_binding, x)) intr_ts) []
||> Sign.restore_naming thy1
--- a/src/HOL/Tools/Function/function_core.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 19:57:46 2009 +0100
@@ -460,7 +460,6 @@
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
- kind = "",
alt_name = Binding.empty,
coind = false,
no_elim = false,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 19:57:46 2009 +0100
@@ -355,9 +355,8 @@
thy
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = "",
- alt_name = Binding.empty, coind = false, no_elim = false,
- no_ind = false, skip_mono = false, fork_mono = false}
+ {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
+ no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
(map (fn (s, T) =>
((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
pnames
--- a/src/HOL/Tools/inductive.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/inductive.ML Fri Nov 13 19:57:46 2009 +0100
@@ -39,8 +39,8 @@
val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
thm list list * local_theory
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
- coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
+ {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
+ no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
val add_inductive_i:
inductive_flags -> ((binding * typ) * mixfix) list ->
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
@@ -71,7 +71,7 @@
term list -> (Attrib.binding * term) list -> thm list ->
term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory
- val declare_rules: string -> binding -> bool -> bool -> string list ->
+ val declare_rules: binding -> bool -> bool -> string list ->
thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
thm -> local_theory -> thm list * thm list * thm * local_theory
val add_ind_def: add_ind_def
@@ -509,7 +509,8 @@
fun mk_ind_prem r =
let
- fun subst s = (case dest_predicate cs params s of
+ fun subst s =
+ (case dest_predicate cs params s of
SOME (_, i, ys, (_, Ts)) =>
let
val k = length Ts;
@@ -520,10 +521,11 @@
HOLogic.mk_binop inductive_conj_name
(list_comb (incr_boundvars k s, bs), P))
in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
- | NONE => (case s of
- (t $ u) => (fst (subst t) $ fst (subst u), NONE)
- | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
- | _ => (s, NONE)));
+ | NONE =>
+ (case s of
+ (t $ u) => (fst (subst t) $ fst (subst u), NONE)
+ | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
+ | _ => (s, NONE)));
fun mk_prem s prems =
(case subst s of
@@ -618,16 +620,17 @@
SOME (_, i, ts, (Ts, Us)) =>
let
val l = length Us;
- val zs = map Bound (l - 1 downto 0)
+ val zs = map Bound (l - 1 downto 0);
in
list_abs (map (pair "z") Us, list_comb (p,
make_bool_args' bs i @ make_args argTs
((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
end
- | NONE => (case t of
- t1 $ t2 => subst t1 $ subst t2
- | Abs (x, T, u) => Abs (x, T, subst u)
- | _ => t));
+ | NONE =>
+ (case t of
+ t1 $ t2 => subst t1 $ subst t2
+ | Abs (x, T, u) => Abs (x, T, subst u)
+ | _ => t));
(* transform an introduction rule into a conjunction *)
(* [| p_i t; ... |] ==> p_j u *)
@@ -698,8 +701,8 @@
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
-fun declare_rules kind rec_binding coind no_ind cnames
- intrs intr_bindings intr_atts elims raw_induct lthy =
+fun declare_rules rec_binding coind no_ind cnames
+ intrs intr_bindings intr_atts elims raw_induct lthy =
let
val rec_name = Binding.name_of rec_binding;
fun rec_qualified qualified = Binding.qualify qualified rec_name;
@@ -716,7 +719,7 @@
val (intrs', lthy1) =
lthy |>
- LocalTheory.notes kind
+ LocalTheory.notes ""
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
map (fn th => [([th],
[Attrib.internal (K (Context_Rules.intro_query NONE)),
@@ -724,16 +727,16 @@
map (hd o snd);
val (((_, elims'), (_, [induct'])), lthy2) =
lthy1 |>
- LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
+ LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
- LocalTheory.note kind
+ LocalTheory.note ""
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
[Attrib.internal (K (Rule_Cases.case_names cases)),
Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),
Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
- LocalTheory.note kind
+ LocalTheory.note ""
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
@@ -742,7 +745,7 @@
else
let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
lthy2 |>
- LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
+ LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []),
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
Attrib.internal (K (Rule_Cases.consumes 1)),
@@ -751,8 +754,8 @@
in (intrs', elims', induct', lthy3) end;
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
- coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
+ {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
+ no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
type add_ind_def =
inductive_flags ->
@@ -760,8 +763,7 @@
term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory;
-fun add_ind_def
- {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn lthy =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -797,7 +799,7 @@
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
rec_preds_defs lthy1);
- val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind
+ val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
cnames intrs intr_names intr_atts elims raw_induct lthy1;
val result =
@@ -817,7 +819,7 @@
(* external interfaces *)
fun gen_add_inductive_i mk_def
- (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
+ (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
cnames_syn pnames spec monos lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -880,9 +882,8 @@
|> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
val (cs, ps) = chop (length cnames_syn) vars;
val monos = Attrib.eval_thms lthy raw_monos;
- val flags = {quiet_mode = false, verbose = verbose, kind = "",
- alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
- skip_mono = false, fork_mono = not int};
+ val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
+ coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
in
lthy
|> LocalTheory.set_group (serial ())
--- a/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 17:15:35 2009 +0000
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 19:57:46 2009 +0100
@@ -351,8 +351,8 @@
val (ind_info, thy3') = thy2 |>
Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
- coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+ {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
+ no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
--- 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)