# HG changeset patch
# User wenzelm
# Date 1268675956 -3600
# Node ID fd1bb29f81700959b042310145c2fc2f10345870
# Parent  533dd944e29ca70d049a0dcae76c4869323b1d2c
replaced type_syntax/term_syntax by uniform syntax_declaration;

diff -r 533dd944e29c -r fd1bb29f8170 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Mar 15 15:13:22 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Mar 15 18:59:16 2010 +0100
@@ -772,7 +772,7 @@
 
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
-          (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
+          (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
       |> Theory_Target.init (SOME name)
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
diff -r 533dd944e29c -r fd1bb29f8170 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Mar 15 15:13:22 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Mar 15 18:59:16 2010 +0100
@@ -39,9 +39,8 @@
     local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * 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 syntax_declaration: bool -> declaration -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val class_alias: binding -> class -> local_theory -> local_theory
@@ -72,9 +71,8 @@
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * 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,
+  syntax_declaration: bool -> declaration -> local_theory -> local_theory,
   reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -195,9 +193,8 @@
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
 val define = apsnd checkpoint oo operation1 #define;
 val notes_kind = apsnd checkpoint ooo operation2 #notes;
-val type_syntax = checkpoint ooo operation2 #type_syntax;
-val term_syntax = checkpoint ooo operation2 #term_syntax;
 val declaration = checkpoint ooo operation2 #declaration;
+val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -207,24 +204,24 @@
 
 fun type_notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
-  in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
+  in syntax_declaration false (ProofContext.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 term_syntax false (ProofContext.target_notation add mode args) lthy end;
+  in syntax_declaration false (ProofContext.target_notation add mode args) lthy end;
 
 
 (* name space aliases *)
 
-fun alias syntax_declaration global_alias local_alias b name =
+fun alias global_alias local_alias b name =
   syntax_declaration 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;
 
-val class_alias = alias type_syntax Sign.class_alias ProofContext.class_alias;
-val type_alias = alias type_syntax Sign.type_alias ProofContext.type_alias;
-val const_alias = alias term_syntax Sign.const_alias ProofContext.const_alias;
+val class_alias = alias Sign.class_alias ProofContext.class_alias;
+val type_alias = alias Sign.type_alias ProofContext.type_alias;
+val const_alias = alias Sign.const_alias ProofContext.const_alias;
 
 
 (* init *)
diff -r 533dd944e29c -r fd1bb29f8170 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 15 15:13:22 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 15 18:59:16 2010 +0100
@@ -33,7 +33,7 @@
     (string * sort) list * ((string * typ) * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
-    declaration list * declaration list ->
+    declaration list ->
     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
@@ -44,14 +44,12 @@
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
   val specification_of: theory -> string -> term option * term list
-  val declarations_of: theory -> string -> declaration list * declaration list
 
   (* Storing results *)
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
-  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
+  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -97,26 +95,27 @@
   intros: thm option * thm option,
   axioms: thm list,
   (** dynamic part **)
-  decls: (declaration * stamp) list * (declaration * stamp) list,
-    (* type and term syntax declarations *)
+  syntax_decls: (declaration * stamp) list,
+    (* syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
     (* theorem declarations *)
   dependencies: ((string * morphism) * stamp) list
     (* locale dependencies (sublocale relation) *)
 };
 
-fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
+fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
-    decls = decls, notes = notes, dependencies = dependencies};
+    syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
+
+fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
+  mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
 
-fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
-  mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
-
-fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
-  notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
-    dependencies = dependencies', ...}) = mk_locale
+fun merge_locale
+ (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
+  Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
+    mk_locale
       ((parameters, spec, intros, axioms),
-        (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+        ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
           merge (eq_snd op =) (notes, notes')),
             merge (eq_snd op =) (dependencies, dependencies')));
 
@@ -139,11 +138,11 @@
     SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name));
 
-fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
+fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
-        ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
+        ((map (fn decl => (decl, stamp ())) syntax_decls, map (fn n => (n, stamp ())) notes),
           map (fn d => (d, stamp ())) dependencies))) #> snd);
 
 fun change_locale name =
@@ -167,9 +166,6 @@
 
 fun specification_of thy = #spec o the_locale thy;
 
-fun declarations_of thy name = the_locale thy name |>
-  #decls |> pairself (map fst);
-
 fun dependencies_of thy name = the_locale thy name |>
   #dependencies |> map fst;
 
@@ -257,14 +253,13 @@
 
 (* Declarations, facts and entire locale content *)
 
-fun activate_decls (name, morph) context =
+fun activate_syntax_decls (name, morph) context =
   let
     val thy = Context.theory_of context;
-    val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
+    val {syntax_decls, ...} = the_locale thy name;
   in
     context
-    |> fold_rev (fn (decl, _) => decl morph) typ_decls
-    |> fold_rev (fn (decl, _) => decl morph) term_decls
+    |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   end;
 
 fun activate_notes activ_elem transfer thy (name, morph) input =
@@ -300,7 +295,10 @@
 fun activate_declarations dep = Context.proof_map (fn context =>
   let
     val thy = Context.theory_of context;
-  in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
+  in
+    roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
+    |-> put_idents
+  end);
 
 fun activate_facts dep context =
   let
@@ -512,23 +510,15 @@
 
 (* Declarations *)
 
-local
-
-fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
-
-fun add_decls add loc decl =
-  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
+fun add_declaration loc decl =
   add_thmss loc ""
-    [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
+    [((Binding.conceal Binding.empty,
+        [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
-in
-
-val add_type_syntax = add_decls (apfst o cons);
-val add_term_syntax = add_decls (apsnd o cons);
-val add_declaration = add_decls (K I);
-
-end;
+fun add_syntax_declaration loc decl =
+  ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, stamp ())))
+  #> add_declaration loc decl;
 
 
 (*** Reasoning about locales ***)
diff -r 533dd944e29c -r fd1bb29f8170 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Mar 15 15:13:22 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Mar 15 18:59:16 2010 +0100
@@ -99,9 +99,8 @@
 
 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;
+val syntax_declaration = target_decl Locale.add_syntax_declaration;
 
 end;
 
@@ -229,7 +228,7 @@
         Local_Theory.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 false (locale_const ta prmode ((b, mx2), lhs')) #>
+            syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
             is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else
@@ -277,7 +276,7 @@
     val t = Term.list_comb (const, params);
   in
     lthy'
-    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
+    |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
     |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     |> Local_Defs.add_def ((b, NoSyn), t)
   end;
@@ -354,9 +353,8 @@
     abbrev = abbrev ta,
     define = define ta,
     notes = notes ta,
-    type_syntax = type_syntax ta,
-    term_syntax = term_syntax ta,
     declaration = declaration ta,
+    syntax_declaration = syntax_declaration ta,
     reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
     exit = Local_Theory.target_of o
       (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation