# HG changeset patch
# User wenzelm
# Date 1185648024 -7200
# Node ID ed4d7abffee7e9abbff5a993823814f176d156f8
# Parent  67bde7cfcf10e09ed5233d60da154cd8708b0aec
tuned signature;

diff -r 67bde7cfcf10 -r ed4d7abffee7 src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Jul 28 20:40:22 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Jul 28 20:40:24 2007 +0200
@@ -16,8 +16,7 @@
   val funs: thm -> {is_const: morphism -> cterm -> bool,
     dest_const: morphism -> cterm -> Rat.rat,
     mk_const: morphism -> ctyp -> Rat.rat -> cterm,
-    conv: morphism -> Proof.context -> cterm -> thm} ->
-      morphism -> Context.generic -> Context.generic
+    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
   val setup: theory -> theory
 end;
 
diff -r 67bde7cfcf10 -r ed4d7abffee7 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Jul 28 20:40:22 2007 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Jul 28 20:40:24 2007 +0200
@@ -16,8 +16,7 @@
   val funs: thm -> 
     {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
      whatis: morphism -> cterm -> cterm -> ord,
-     simpset: morphism -> simpset}
-             -> morphism -> Context.generic -> Context.generic
+     simpset: morphism -> simpset} -> declaration
   val match: Proof.context -> cterm -> entry option
   val setup: theory -> theory
 end;
diff -r 67bde7cfcf10 -r ed4d7abffee7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Jul 28 20:40:22 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 28 20:40:24 2007 +0200
@@ -233,9 +233,8 @@
 (* declarations *)
 
 val declaration =
-  ML_Context.use_let
-    "val declaration: Morphism.morphism -> Context.generic -> Context.generic"
-  "Context.map_proof (LocalTheory.declaration declaration)"
+  ML_Context.use_let "val declaration: declaration"
+    "Context.map_proof (LocalTheory.declaration declaration)"
   #> Context.proof_map;
 
 
diff -r 67bde7cfcf10 -r ed4d7abffee7 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jul 28 20:40:22 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Jul 28 20:40:24 2007 +0200
@@ -6,6 +6,7 @@
 *)
 
 type local_theory = Proof.context;
+type declaration = morphism -> Context.generic -> Context.generic;
 
 signature LOCAL_THEORY =
 sig
@@ -31,9 +32,9 @@
     local_theory -> (term * (bstring * thm)) list * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory
-  val type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
-  val term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
-  val declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> 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 def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory
   val note: string -> (bstring * Attrib.src list) * thm list ->
@@ -67,9 +68,9 @@
   notes: string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory,
-  type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
-  term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
-  declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
+  type_syntax: declaration -> local_theory -> local_theory,
+  term_syntax: declaration -> local_theory -> local_theory,
+  declaration: declaration -> local_theory -> local_theory,
   target_morphism: local_theory -> morphism,
   target_naming: local_theory -> NameSpace.naming,
   reinit: local_theory -> theory -> local_theory,
diff -r 67bde7cfcf10 -r ed4d7abffee7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jul 28 20:40:22 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 28 20:40:24 2007 +0200
@@ -94,12 +94,9 @@
   val add_thmss: string -> string ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-  val add_type_syntax: string -> (morphism -> Context.generic -> Context.generic) ->
-    Proof.context -> Proof.context
-  val add_term_syntax: string -> (morphism -> Context.generic -> Context.generic) ->
-    Proof.context -> Proof.context
-  val add_declaration: string -> (morphism -> Context.generic -> Context.generic) ->
-    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 interpretation_i: (Proof.context -> Proof.context) ->
     (bool * string) * Attrib.src list -> expr ->
@@ -166,7 +163,7 @@
 fun map_elem f (Elem e) = Elem (f e)
   | map_elem _ (Expr e) = Expr e;
 
-type decl = (morphism -> Context.generic -> Context.generic) * stamp;
+type decl = declaration * stamp;
 
 type locale =
  {axiom: Element.witness list,