# HG changeset patch
# User wenzelm
# Date 1319833050 -7200
# Node ID 57cd50f98fdcbee3decfcb3559b648a2a25814d5
# Parent  f599ac41e7f57dcf4f4517a4e049b0d44d44976b
uniform Local_Theory.declaration with explicit params;

diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -340,7 +340,7 @@
 fun add_declaration name decl thy =
   thy
   |> Named_Target.init I name
-  |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
+  |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -128,7 +128,8 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
-         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
+         lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
+          (add_function_data o transform_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -203,7 +204,8 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
+               |> Local_Theory.declaration {syntax = false, pervasive = false}
+                 (add_function_data o transform_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -75,7 +75,7 @@
     fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
     fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
     val lthy'' =
-      Local_Theory.declaration true
+      Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
   in
     (qconst_data, lthy'')
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -143,7 +143,7 @@
     fun qinfo phi = Quotient_Info.transform_quotients phi quotients
 
     val lthy4 = lthy3
-      |> Local_Theory.declaration true
+      |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/enriched_type.ML
--- a/src/HOL/Tools/enriched_type.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -240,7 +240,8 @@
         |> Local_Theory.note ((qualify identityN, []),
             [prove_identity lthy id_thm])
         |> snd
-        |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm))
+        |> Local_Theory.declaration {syntax = false, pervasive = false}
+          (mapper_declaration comp_thm id_thm))
   in
     lthy
     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -931,7 +931,7 @@
        eqs = eqs'};
 
     val lthy4 = lthy3
-      |> Local_Theory.declaration false (fn phi =>
+      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
         let val result' = transform_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, lthy4) end;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/typedef.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -247,7 +247,8 @@
           Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
       in
         lthy2
-        |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
+        |> Local_Theory.declaration {syntax = false, pervasive = true}
+          (fn phi => put_info full_tname (transform_info phi info))
         |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
         |> pair (full_tname, info)
       end;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -561,7 +561,6 @@
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
-        syntax_declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -202,9 +202,8 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
-    ("Context.map_proof (Local_Theory." ^
-      (if syntax then "syntax_declaration" else "declaration") ^ " " ^
-      Bool.toString pervasive ^ " declaration)")
+    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
+      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   |> Context.proof_map;
 
 
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -39,8 +39,7 @@
     local_theory -> (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val declaration: bool -> declaration -> local_theory -> local_theory
-  val syntax_declaration: bool -> declaration -> local_theory -> local_theory
+  val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
@@ -71,8 +70,7 @@
     local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
-  declaration: bool -> declaration -> local_theory -> local_theory,
-  syntax_declaration: bool -> declaration -> local_theory -> local_theory,
+  declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list,
   exit: local_theory -> Proof.context};
 
@@ -200,7 +198,6 @@
 val define = apsnd checkpoint oo operation1 #define;
 val notes_kind = apsnd checkpoint ooo operation2 #notes;
 val declaration = checkpoint ooo operation2 #declaration;
-val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
 
 
 
@@ -210,24 +207,29 @@
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
 fun set_defsort S =
-  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
+  declaration {syntax = true, pervasive = false}
+    (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
 (* notation *)
 
 fun type_notation add mode raw_args lthy =
-  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
-  in syntax_declaration false (Proof_Context.target_type_notation add mode args) lthy end;
+  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
+    declaration {syntax = true, pervasive = false}
+      (Proof_Context.target_type_notation add mode args) lthy
+  end;
 
 fun notation add mode raw_args lthy =
-  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
-  in syntax_declaration false (Proof_Context.target_notation add mode args) lthy end;
+  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
+    declaration {syntax = true, pervasive = false}
+      (Proof_Context.target_notation add mode args) lthy
+  end;
 
 
 (* name space aliases *)
 
 fun alias global_alias local_alias b name =
-  syntax_declaration false (fn phi =>
+  declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end)
   #> local_alias b name;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -56,9 +56,9 @@
     |> Local_Theory.target (add locale locale_decl)
   end;
 
-fun target_declaration (Target {target, ...}) {syntax, pervasive} =
+fun target_declaration (Target {target, ...}) params =
   if target = "" then Generic_Target.theory_declaration
-  else locale_declaration target {syntax = syntax, pervasive = pervasive};
+  else locale_declaration target params;
 
 
 (* consts in locales *)
@@ -193,10 +193,7 @@
        {define = Generic_Target.define (target_foundation ta),
         notes = Generic_Target.notes (target_notes ta),
         abbrev = Generic_Target.abbrev (target_abbrev ta),
-        declaration = fn pervasive => target_declaration ta
-          {syntax = false, pervasive = pervasive},
-        syntax_declaration = fn pervasive => target_declaration ta
-          {syntax = true, pervasive = pervasive},
+        declaration = target_declaration ta,
         pretty = pretty ta,
         exit = Local_Theory.target_of o before_exit}
   end;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -207,7 +207,6 @@
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
-        syntax_declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -50,7 +50,7 @@
   let
     val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
   in
-    lthy |> Local_Theory.declaration true
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi =>
         let
           val (ts', ths') =
diff -r f599ac41e7f5 -r 57cd50f98fdc src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -192,7 +192,7 @@
        proc = proc,
        identifier = identifier};
   in
-    lthy |> Local_Theory.declaration false (fn phi => fn context =>
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;