# HG changeset patch
# User wenzelm
# Date 1257499573 -3600
# Node ID 8f2e102f6628fa0784051b46cfd649cb488fcd09
# Parent  8c489493e65ea68d4681463e5f7b484d3ae6a72a# Parent  a4a38ed813f766ce0042ec6a597ed478ba54b27e
merged

diff -r 8c489493e65e -r 8f2e102f6628 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -355,7 +355,7 @@
 fun add_declaration name decl thy =
   thy
   |> TheoryTarget.init name
-  |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
+  |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
   |> LocalTheory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
diff -r 8c489493e65e -r 8f2e102f6628 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -338,8 +338,7 @@
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
   in
     thy2
-    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
-       o Context.Theory
+    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
     |> Sign.parent_path
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
diff -r 8c489493e65e -r 8f2e102f6628 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -118,7 +118,7 @@
             else Specification.print_consts lthy (K false) (map fst fixes)
         in
           lthy
-          |> LocalTheory.declaration (add_function_data o morph_function_data cdata)
+          |> LocalTheory.declaration false (add_function_data o morph_function_data cdata)
         end
     in
       lthy
diff -r 8c489493e65e -r 8f2e102f6628 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -20,9 +20,11 @@
 
 signature BASIC_INDUCTIVE =
 sig
-  type inductive_result
+  type inductive_result =
+    {preds: term list, elims: thm list, raw_induct: thm,
+     induct: thm, intrs: thm list}
   val morph_result: morphism -> inductive_result -> inductive_result
-  type inductive_info
+  type inductive_info = {names: string list, coind: bool} * inductive_result
   val the_inductive: Proof.context -> string -> inductive_info
   val print_inductives: Proof.context -> unit
   val mono_add: attribute
@@ -36,7 +38,9 @@
     thm list list * local_theory
   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     thm list list * local_theory
-  type inductive_flags
+  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}
   val add_inductive_i:
     inductive_flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
@@ -62,7 +66,11 @@
 signature INDUCTIVE =
 sig
   include BASIC_INDUCTIVE
-  type add_ind_def
+  type add_ind_def =
+    inductive_flags ->
+    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 ->
     thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
@@ -592,19 +600,21 @@
 
 (** specification of (co)inductive predicates **)
 
-fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
-  let  (* FIXME proper naming convention: lthy *)
+fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
+    cs intr_ts monos params cnames_syn lthy =
+  let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
     val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
     val k = log 2 1 (length cs);
     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
-    val p :: xs = map Free (Variable.variant_frees ctxt intr_ts
+    val p :: xs = map Free (Variable.variant_frees lthy intr_ts
       (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
-    val bs = map Free (Variable.variant_frees ctxt (p :: xs @ intr_ts)
+    val bs = map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
       (map (rpair HOLogic.boolT) (mk_names "b" k)));
 
-    fun subst t = (case dest_predicate cs params t of
+    fun subst t =
+      (case dest_predicate cs params t of
         SOME (_, i, ts, (Ts, Us)) =>
           let
             val l = length Us;
@@ -651,44 +661,44 @@
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
-    val ((rec_const, (_, fp_def)), ctxt') = ctxt
+    val ((rec_const, (_, fp_def)), lthy') = lthy
       |> LocalTheory.conceal
       |> LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          (Attrib.empty_binding, fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> LocalTheory.restore_naming ctxt;
+      ||> LocalTheory.restore_naming lthy;
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
-      (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
+      (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
     val specs =
       if length cs < 2 then []
       else
         map_index (fn (i, (name_mx, c)) =>
           let
             val Ts = arg_types_of (length params) c;
-            val xs = map Free (Variable.variant_frees ctxt intr_ts
+            val xs = map Free (Variable.variant_frees lthy intr_ts
               (mk_names "x" (length Ts) ~~ Ts))
           in
             (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
               (list_comb (rec_const, params @ make_bool_args' bs i @
                 make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs);
-    val (consts_defs, ctxt'') = ctxt'
+    val (consts_defs, lthy'') = lthy'
       |> LocalTheory.conceal
       |> fold_map (LocalTheory.define Thm.internalK) specs
-      ||> LocalTheory.restore_naming ctxt';
+      ||> LocalTheory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
-    val ((_, [mono']), ctxt''') =
-      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt'';
+    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
+    val ((_, [mono']), lthy''') =
+      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
 
-  in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
+  in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     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 ctxt =
+fun declare_rules kind 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;
@@ -703,86 +713,91 @@
         (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
       else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
 
-    val (intrs', ctxt1) =
-      ctxt |>
+    val (intrs', lthy1) =
+      lthy |>
       LocalTheory.notes kind
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
            [Attrib.internal (K (Context_Rules.intro_query NONE)),
             Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
       map (hd o snd);
-    val (((_, elims'), (_, [induct'])), ctxt2) =
-      ctxt1 |>
+    val (((_, elims'), (_, [induct'])), lthy2) =
+      lthy1 |>
       LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note kind ((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]) #>
+        LocalTheory.note kind
+          ((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
         ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
-    val ctxt3 = if no_ind orelse coind then ctxt2 else
-      let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
-      in
-        ctxt2 |>
-        LocalTheory.notes kind [((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)),
-             Attrib.internal (K (Induct.induct_pred name))])))] |> snd
-      end
-  in (intrs', elims', induct', ctxt3) end;
+    val lthy3 =
+      if no_ind orelse coind then lthy2
+      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"), []),
+            inducts |> map (fn (name, th) => ([th],
+              [Attrib.internal (K ind_case_names),
+               Attrib.internal (K (Rule_Cases.consumes 1)),
+               Attrib.internal (K (Induct.induct_pred name))])))] |> snd
+        end;
+  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}
+   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
 
 type add_ind_def =
   inductive_flags ->
   term list -> (Attrib.binding * term) list -> thm list ->
   term list -> (binding * mixfix) list ->
-  local_theory -> inductive_result * local_theory
+  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}
-    cs intros monos params cnames_syn ctxt =
+fun add_ind_def
+    {quiet_mode, verbose, kind, 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";
     val names = map (Binding.name_of o fst) cnames_syn;
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val cnames = map (LocalTheory.full_name ctxt o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (LocalTheory.full_name lthy o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
-      apfst split_list (split_list (map (check_rule ctxt cs params) intros));
+      apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
-    val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
+    val (lthy1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
       argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
-        monos params cnames_syn ctxt;
+        monos params cnames_syn lthy;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
-      params intr_ts rec_preds_defs ctxt1;
-    val elims = if no_elim then [] else
-      prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
-        unfold rec_preds_defs ctxt1;
+      params intr_ts rec_preds_defs lthy1;
+    val elims =
+      if no_elim then []
+      else
+        prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
+          unfold rec_preds_defs lthy1;
     val raw_induct = zero_var_indexes
-      (if no_ind then Drule.asm_rl else
-       if coind then
+      (if no_ind then Drule.asm_rl
+       else if coind then
          singleton (ProofContext.export
-           (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
+           (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
            (rotate_prems ~1 (ObjectLogic.rulify
              (fold_rule rec_preds_defs
                (rewrite_rule simp_thms'''
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
-           rec_preds_defs ctxt1);
+           rec_preds_defs lthy1);
 
-    val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
-      cnames intrs intr_names intr_atts elims raw_induct ctxt1;
+    val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind
+      cnames intrs intr_names intr_atts elims raw_induct lthy1;
 
     val result =
       {preds = preds,
@@ -791,11 +806,11 @@
        raw_induct = rulify raw_induct,
        induct = induct};
 
-    val ctxt3 = ctxt2
-      |> LocalTheory.declaration (fn phi =>
+    val lthy3 = lthy2
+      |> LocalTheory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
-  in (result, ctxt3) end;
+  in (result, lthy3) end;
 
 
 (* external interfaces *)
@@ -970,8 +985,13 @@
 
 val ind_decl = gen_ind_decl add_ind_def;
 
-val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
-val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
+val _ =
+  OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
+    (ind_decl false);
+
+val _ =
+  OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
+    (ind_decl true);
 
 val _ =
   OuterSyntax.local_theory "inductive_cases"
diff -r 8c489493e65e -r 8f2e102f6628 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -406,11 +406,11 @@
 
 fun add_ind_set_def
     {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
-    cs intros monos params cnames_syn ctxt =
-  let (* FIXME proper naming convention: lthy *)
-    val thy = ProofContext.theory_of ctxt;
+    cs intros monos params cnames_syn lthy =
+  let
+    val thy = ProofContext.theory_of lthy;
     val {set_arities, pred_arities, to_pred_simps, ...} =
-      PredSetConvData.get (Context.Proof ctxt);
+      PredSetConvData.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
       | infer (Const ("op :", _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
@@ -446,9 +446,9 @@
         val (Us, U) = split_last (binder_types T);
         val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
           [Pretty.str "Argument types",
-           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) Us)),
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) Us)),
            Pretty.str ("of " ^ s ^ " do not agree with types"),
-           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) paramTs)),
            Pretty.str "of declared parameters"]));
         val Ts = HOLogic.strip_ptupleT fs U;
         val c' = Free (s ^ "p",
@@ -474,29 +474,29 @@
         Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
         eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
-    val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
-    val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
+    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,
           coind = coind, no_elim = no_elim, no_ind = no_ind,
           skip_mono = skip_mono, fork_mono = fork_mono}
-        cs' intros' monos' params1 cnames_syn' ctxt;
+        cs' intros' monos' params1 cnames_syn' lthy;
 
     (* define inductive sets using previously defined predicates *)
-    val (defs, ctxt2) = ctxt1
+    val (defs, lthy2) = lthy1
       |> LocalTheory.conceal  (* FIXME ?? *)
       |> fold_map (LocalTheory.define Thm.internalK)
         (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
            (cnames_syn ~~ cs_info ~~ preds))
-      ||> LocalTheory.restore_naming ctxt1;
+      ||> LocalTheory.restore_naming lthy1;
 
     (* prove theorems for converting predicate to set notation *)
-    val ctxt3 = fold
-      (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn ctxt =>
+    val lthy3 = fold
+      (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy =>
         let val conv_thm =
-          Goal.prove ctxt (map (fst o dest_Free) params) []
+          Goal.prove lthy (map (fst o dest_Free) params) []
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
               (list_comb (p, params3),
                list_abs (map (pair "x") Ts, HOLogic.mk_mem
@@ -505,29 +505,29 @@
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, split_conv]) 1))
         in
-          ctxt |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
+          lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),
               [conv_thm]) |> snd
-        end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
+        end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
 
     (* convert theorems to set notation *)
     val rec_name =
       if Binding.is_empty alt_name then
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
-    val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (LocalTheory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
-    val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
-    val (intrs', elims', induct, ctxt4) =
+    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
-      (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
-      (map (fn th => (to_set [] (Context.Proof ctxt3) th,
-         map fst (fst (Rule_Cases.get th)))) elims)
-      raw_induct' ctxt3
+        (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)
+        raw_induct' lthy3;
   in
     ({intrs = intrs', elims = elims', induct = induct,
       raw_induct = raw_induct', preds = map fst defs},
-     ctxt4)
+     lthy4)
   end;
 
 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
@@ -544,8 +544,10 @@
 val setup =
   Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
     "declare rules for converting between predicate and set notation" #>
-  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
-  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
+  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
+    "convert rule to set notation" #>
+  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
+    "convert rule to predicate notation" #>
   Attrib.setup @{binding code_ind_set}
     (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
     "introduction rules for executable predicates" #>
@@ -562,10 +564,12 @@
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
 val _ =
-  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
+    (ind_set_decl false);
 
 val _ =
-  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
+    (ind_set_decl true);
 
 end;
 
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -44,7 +44,8 @@
           else ());
     val b = Binding.name c;
 
-    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
+    val head = Const (Sign.full_bname thy c, T);
+    val def = Term.subst_atomic [(Free (c, T), head)] prop;
     val name = Thm.def_binding_optional b raw_name;
     val atts = map (prep_att thy) raw_atts;
 
@@ -52,7 +53,10 @@
       thy
       |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
-      |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
+      |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
+        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
+        Code.add_default_eqn thm #>
+        Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -16,7 +16,7 @@
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
-  val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
+  val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
   val hide_names: bool -> string * xstring list -> theory -> theory
@@ -178,10 +178,10 @@
 
 (* declarations *)
 
-fun declaration (txt, pos) =
+fun declaration pervasive (txt, pos) =
   txt |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
-    "Context.map_proof (LocalTheory.declaration declaration)"
+    ("Context.map_proof (LocalTheory.declaration " ^ Bool.toString pervasive ^ " declaration)")
   |> Context.proof_map;
 
 
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -22,8 +22,9 @@
   "advanced", "and", "assumes", "attach", "begin", "binder",
   "constrains", "defines", "fixes", "for", "identifier", "if",
   "imports", "in", "infix", "infixl", "infixr", "is",
-  "notes", "obtains", "open", "output", "overloaded", "shows",
-  "structure", "unchecked", "uses", "where", "|"];
+  "notes", "obtains", "open", "output", "overloaded", "pervasive",
+  "shows", "structure", "unchecked", "uses", "where", "|"];
+
 
 
 (** init and exit **)
@@ -337,7 +338,7 @@
 
 val _ =
   OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.ML_source >> IsarCmd.declaration);
+    (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
 
 val _ =
   OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -27,6 +27,7 @@
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
+  val global_morphism: local_theory -> morphism
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -35,9 +36,9 @@
   val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
-  val type_syntax: declaration -> local_theory -> local_theory
-  val term_syntax: declaration -> local_theory -> local_theory
-  val declaration: declaration -> local_theory -> local_theory
+  val type_syntax: bool -> declaration -> local_theory -> local_theory
+  val term_syntax: bool -> declaration -> local_theory -> local_theory
+  val declaration: bool -> declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
@@ -65,9 +66,9 @@
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory,
-  type_syntax: declaration -> local_theory -> local_theory,
-  term_syntax: declaration -> local_theory -> local_theory,
-  declaration: declaration -> local_theory -> local_theory,
+  type_syntax: bool -> declaration -> local_theory -> local_theory,
+  term_syntax: bool -> declaration -> local_theory -> local_theory,
+  declaration: bool -> declaration -> local_theory -> local_theory,
   reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -174,27 +175,27 @@
   Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
 
 
 (* basic operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
-fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
 val define = apsnd checkpoint ooo operation2 #define;
 val notes = apsnd checkpoint ooo operation2 #notes;
-val type_syntax = checkpoint oo operation1 #type_syntax;
-val term_syntax = checkpoint oo operation1 #term_syntax;
-val declaration = checkpoint oo operation1 #declaration;
+val type_syntax = checkpoint ooo operation2 #type_syntax;
+val term_syntax = checkpoint ooo operation2 #term_syntax;
+val declaration = checkpoint ooo operation2 #declaration;
 
 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
-  in term_syntax (ProofContext.target_notation add mode args) lthy end;
+  in term_syntax false (ProofContext.target_notation add mode args) lthy end;
 
 
 (* init *)
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -1,18 +1,19 @@
 (*  Title:      Pure/Isar/spec_rules.ML
     Author:     Makarius
 
-Rules that characterize functional/relational specifications.  NB: In
-the face of arbitrary morphisms, the original shape of specifications
-may get transformed almost arbitrarily.
+Rules that characterize specifications, with rough classification.
+NB: In the face of arbitrary morphisms, the original shape of
+specifications may get lost.
 *)
 
 signature SPEC_RULES =
 sig
-  datatype kind = Functional | Relational | Co_Relational
-  val dest: Proof.context -> (kind * (term * thm list) list) list
-  val dest_global: theory -> (kind * (term * thm list) list) list
-  val add: kind * (term * thm list) list -> local_theory -> local_theory
-  val add_global: kind * (term * thm list) list -> theory -> theory
+  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
+  type spec = rough_classification * (term list * thm list)
+  val get: Proof.context -> spec list
+  val get_global: theory -> spec list
+  val add: rough_classification -> term list * thm list -> local_theory -> local_theory
+  val add_global: rough_classification -> term list * thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =
@@ -20,30 +21,34 @@
 
 (* maintain rules *)
 
-datatype kind = Functional | Relational | Co_Relational;
+datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
+type spec = rough_classification * (term list * thm list);
 
 structure Rules = GenericDataFun
 (
-  type T = (kind * (term * thm list) list) Item_Net.T;
+  type T = spec Item_Net.T;
   val empty : T =
     Item_Net.init
-      (fn ((k1, spec1), (k2, spec2)) => k1 = k2 andalso
-        eq_list (fn ((t1, ths1), (t2, ths2)) =>
-          t1 aconv t2 andalso eq_list Thm.eq_thm_prop (ths1, ths2)) (spec1, spec2))
-      (map #1 o #2);
+      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
+        class1 = class2 andalso
+        eq_list (op aconv) (ts1, ts2) andalso
+        eq_list Thm.eq_thm_prop (ths1, ths2))
+      (#1 o #2);
   val extend = I;
   fun merge _ = Item_Net.merge;
 );
 
-val dest = Item_Net.content o Rules.get o Context.Proof;
-val dest_global = Item_Net.content o Rules.get o Context.Theory;
+val get = Item_Net.content o Rules.get o Context.Proof;
+val get_global = Item_Net.content o Rules.get o Context.Theory;
 
-fun add (kind, specs) = LocalTheory.declaration
+fun add class (ts, ths) = LocalTheory.declaration true
   (fn phi =>
-    let val specs' = map (fn (t, ths) => (Morphism.term phi t, Morphism.fact phi ths)) specs;
-    in Rules.map (Item_Net.update (kind, specs')) end);
+    let
+      val ts' = map (Morphism.term phi) ts;
+      val ths' = map (Morphism.thm phi) ths;
+    in Rules.map (Item_Net.update (class, (ts', ths'))) end);
 
-fun add_global entry =
-  Context.theory_map (Rules.map (Item_Net.update entry));
+fun add_global class spec =
+  Context.theory_map (Rules.map (Item_Net.update (class, spec)));
 
 end;
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -201,19 +201,23 @@
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val name = Thm.def_binding_optional b raw_name;
-    val ((lhs, (_, th)), lthy2) = lthy
+    val ((lhs, (_, raw_th)), lthy2) = lthy
       |> LocalTheory.define Thm.definitionK
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
-    val ((def_name, [th']), lthy3) = lthy2
+
+    val th = prove lthy2 raw_th;
+    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
+
+    val ((def_name, [th']), lthy4) = lthy3
       |> LocalTheory.note Thm.definitionK
-        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: Code.add_default_eqn_attrib :: atts),
-          [prove lthy2 th]);
+        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
+            Code.add_default_eqn_attrib :: atts), [th]);
 
-    val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
+    val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
     val _ =
       if not do_print then ()
-      else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
-  in ((lhs, (def_name, th')), lthy3) end;
+      else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+  in ((lhs, (def_name, th')), lthy4) end;
 
 val definition = gen_def false check_free_spec;
 val definition_cmd = gen_def true read_free_spec;
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -71,26 +71,38 @@
      else pretty_thy ctxt target is_class);
 
 
-(* target declarations *)
+(* generic declarations *)
+
+local
 
-fun target_decl add (Target {target, ...}) d lthy =
+fun direct_decl decl =
+  let val decl0 = Morphism.form decl in
+    LocalTheory.theory (Context.theory_map decl0) #>
+    LocalTheory.target (Context.proof_map decl0)
+  end;
+
+fun target_decl add (Target {target, ...}) pervasive decl lthy =
   let
-    val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
-    val d0 = Morphism.form d';
+    val global_decl = Morphism.transform (LocalTheory.global_morphism lthy) decl;
+    val target_decl = Morphism.transform (LocalTheory.target_morphism lthy) decl;
   in
     if target = "" then
       lthy
-      |> LocalTheory.theory (Context.theory_map d0)
-      |> LocalTheory.target (Context.proof_map d0)
+      |> direct_decl target_decl
     else
       lthy
-      |> LocalTheory.target (add target d')
+      |> pervasive ? direct_decl global_decl
+      |> LocalTheory.target (add target target_decl)
   end;
 
+in
+
 val type_syntax = target_decl Locale.add_type_syntax;
 val term_syntax = target_decl Locale.add_term_syntax;
 val declaration = target_decl Locale.add_declaration;
 
+end;
+
 fun class_target (Target {target, ...}) f =
   LocalTheory.raw_theory f #>
   LocalTheory.target (Class_Target.refresh_syntax target);
@@ -221,7 +233,7 @@
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
-    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
+    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
     |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
@@ -246,7 +258,7 @@
         LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
-            term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
+            term_syntax ta false (locale_const ta prmode ((b, mx2), lhs')) #>
             is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      Pure/Tools/named_thms.ML
     Author:     Makarius
 
-Named collections of theorems in canonical order.  Based on naive data
-structures -- not scalable!
+Named collections of theorems in canonical order.
 *)
 
 signature NAMED_THMS =
@@ -20,22 +19,23 @@
 
 structure Data = GenericDataFun
 (
-  type T = thm list;
-  val empty = [];
+  type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
   val extend = I;
-  fun merge _ = Thm.merge_thms;
+  fun merge _ = Item_Net.merge;
 );
 
-val get = Data.get o Context.Proof;
+val content = Item_Net.content o Data.get;
+val get = content o Context.Proof;
 
-val add_thm = Data.map o Thm.add_thm;
-val del_thm = Data.map o Thm.del_thm;
+val add_thm = Data.map o Item_Net.update;
+val del_thm = Data.map o Item_Net.remove;
 
 val add = Thm.declaration_attribute add_thm;
 val del = Thm.declaration_attribute del_thm;
 
 val setup =
   Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
-  PureThy.add_thms_dynamic (Binding.name name, Data.get);
+  PureThy.add_thms_dynamic (Binding.name name, content);
 
 end;
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/more_thm.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -48,6 +48,7 @@
   val add_thm: thm -> thm list -> thm list
   val del_thm: thm -> thm list -> thm list
   val merge_thms: thm list * thm list -> thm list
+  val full_rules: thm Item_Net.T
   val intro_rules: thm Item_Net.T
   val elim_rules: thm Item_Net.T
   val elim_implies: thm -> thm -> thm
@@ -246,6 +247,7 @@
 val del_thm = remove eq_thm_prop;
 val merge_thms = merge eq_thm_prop;
 
+val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
 val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
 val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
 
diff -r 8c489493e65e -r 8f2e102f6628 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Nov 06 09:27:20 2009 +0100
+++ b/src/Pure/simplifier.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -192,7 +192,7 @@
        identifier = identifier}
       |> morph_simproc (LocalTheory.target_morphism lthy);
   in
-    lthy |> LocalTheory.declaration (fn phi =>
+    lthy |> LocalTheory.declaration false (fn phi =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;