--- a/src/HOL/Nominal/nominal_datatype.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Nov 17 14:51:57 2009 +0100
@@ -568,7 +568,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
thy3
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{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))
@@ -1511,7 +1511,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{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))
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Nov 17 14:51:57 2009 +0100
@@ -239,7 +239,7 @@
local
-fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
+fun gen_primrec prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
let
val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
val fixes = List.take (fixes', length raw_fixes);
@@ -280,7 +280,6 @@
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
val (defs_thms, lthy') = lthy |>
- set_group ? Local_Theory.set_group (serial ()) |>
fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
val qualify = Binding.qualify false
(space_implode "_" (map (Long_Name.base_name o #1) defs));
@@ -384,8 +383,8 @@
in
-val add_primrec = gen_primrec false Specification.check_spec (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
+val add_primrec = gen_primrec Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
end;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 17 14:51:57 2009 +0100
@@ -155,7 +155,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{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))
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 17 14:51:57 2009 +0100
@@ -174,7 +174,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
thy1
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{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') []
--- a/src/HOL/Tools/Function/fun.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Tue Nov 17 14:51:57 2009 +0100
@@ -151,15 +151,11 @@
domintros=false, partials=false, tailrec=false }
fun gen_fun add config fixes statements int lthy =
- let val group = serial () in
- lthy
- |> Local_Theory.set_group group
- |> add fixes statements config
- |> by_pat_completeness_auto int
- |> Local_Theory.restore
- |> Local_Theory.set_group group
- |> termination_by (Function_Common.get_termination_prover lthy) int
- end;
+ lthy
+ |> add fixes statements config
+ |> by_pat_completeness_auto int
+ |> Local_Theory.restore
+ |> termination_by (Function_Common.get_termination_prover lthy) int
val add_fun = gen_fun Function.add_function
val add_fun_cmd = gen_fun Function.add_function_cmd
--- a/src/HOL/Tools/Function/function.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Nov 17 14:51:57 2009 +0100
@@ -20,8 +20,6 @@
val termination_proof : term option -> local_theory -> Proof.state
val termination_proof_cmd : string option -> local_theory -> Proof.state
- val termination : term option -> local_theory -> Proof.state
- val termination_cmd : string option -> local_theory -> Proof.state
val setup : theory -> theory
val get_congs : Proof.context -> thm list
@@ -119,7 +117,6 @@
end
in
lthy
- |> is_external ? Local_Theory.set_group (serial ())
|> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
end
@@ -170,18 +167,8 @@
|> Proof.theorem_i NONE afterqed [[(goal, [])]]
end
-val termination_proof = gen_termination_proof Syntax.check_term;
-val termination_proof_cmd = gen_termination_proof Syntax.read_term;
-
-fun termination term_opt lthy =
- lthy
- |> Local_Theory.set_group (serial ())
- |> termination_proof term_opt;
-
-fun termination_cmd term_opt lthy =
- lthy
- |> Local_Theory.set_group (serial ())
- |> termination_proof_cmd term_opt;
+val termination_proof = gen_termination_proof Syntax.check_term
+val termination_proof_cmd = gen_termination_proof Syntax.read_term
(* Datatype hook to declare datatype congs as "function_congs" *)
@@ -217,13 +204,13 @@
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(function_parser default_config
- >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
+ >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd);
+ (Scan.option P.term >> termination_proof_cmd)
-end;
+end
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Nov 17 14:51:57 2009 +0100
@@ -354,7 +354,7 @@
val (ind_result, thy') =
thy
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> 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}
(map (fn (s, T) =>
--- a/src/HOL/Tools/inductive.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Nov 17 14:51:57 2009 +0100
@@ -51,7 +51,7 @@
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
- val add_inductive_global: serial -> inductive_flags ->
+ val add_inductive_global: inductive_flags ->
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
@@ -886,19 +886,17 @@
coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
in
lthy
- |> Local_Theory.set_group (serial ())
|> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
end;
val add_inductive_i = gen_add_inductive_i add_ind_def;
val add_inductive = gen_add_inductive add_ind_def;
-fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
+fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
let
val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
val ctxt' = thy
|> Theory_Target.init NONE
- |> Local_Theory.set_group group
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
|> Local_Theory.exit;
val info = #2 (the_inductive ctxt' name);
--- a/src/HOL/Tools/inductive_realizer.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Nov 17 14:51:57 2009 +0100
@@ -350,7 +350,7 @@
(** realizability predicate **)
val (ind_info, thy3') = thy2 |>
- Inductive.add_inductive_global (serial ())
+ 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}
rlzpreds rlzparams (map (fn (rintr, intr) =>
--- a/src/HOL/Tools/primrec.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/primrec.ML Tue Nov 17 14:51:57 2009 +0100
@@ -265,7 +265,7 @@
local
-fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec prep_spec raw_fixes raw_spec lthy =
let
val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
@@ -275,7 +275,6 @@
map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
in
lthy
- |> set_group ? Local_Theory.set_group (serial ())
|> add_primrec_simple fixes (map snd spec)
|-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
#-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
@@ -284,8 +283,8 @@
in
-val add_primrec = gen_primrec false Specification.check_spec;
-val add_primrec_cmd = gen_primrec true Specification.read_spec;
+val add_primrec = gen_primrec Specification.check_spec;
+val add_primrec_cmd = gen_primrec Specification.read_spec;
end;
--- a/src/HOLCF/Tools/fixrec.ML Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Tue Nov 17 14:51:57 2009 +0100
@@ -421,7 +421,6 @@
(* code adapted from HOL/Tools/primrec.ML *)
fun gen_fixrec
- (set_group : bool)
prep_spec
(strict : bool)
raw_fixes
@@ -473,8 +472,8 @@
in
-val add_fixrec = gen_fixrec false Specification.check_spec;
-val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
+val add_fixrec = gen_fixrec Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec Specification.read_spec;
end; (* local *)