--- 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,