# HG changeset patch
# User wenzelm
# Date 1258465917 -3600
# Node ID 0878aecbf11928d20a487957a6398e5fede81a11
# Parent  a8481da77270dc9a62b369b9bf04d35c385e2686
eliminated slightly odd name space grouping -- now managed by Isar toplevel;

diff -r a8481da77270 -r 0878aecbf119 src/HOL/Nominal/nominal_datatype.ML
--- 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))
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Nominal/nominal_primrec.ML
--- 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;
 
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- 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))
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- 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') []
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Function/fun.ML
--- 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
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Function/function.ML
--- 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
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- 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) =>
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/inductive.ML
--- 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);
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/inductive_realizer.ML
--- 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) =>
diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/primrec.ML
--- 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;
 
diff -r a8481da77270 -r 0878aecbf119 src/HOLCF/Tools/fixrec.ML
--- 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 *)