# HG changeset patch
# User wenzelm
# Date 1185652866 -7200
# Node ID e94e541346d7a24c85c9051d3b9dbd2d86954b96
# Parent  d39d64d96e7163226e8f5a18b29d47dbcab61615
type Morphism.declaration;

diff -r d39d64d96e71 -r e94e541346d7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Jul 28 22:01:01 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 28 22:01:06 2007 +0200
@@ -233,7 +233,7 @@
 (* declarations *)
 
 val declaration =
-  ML_Context.use_let "val declaration: declaration"
+  ML_Context.use_let "val declaration: Morphism.declaration"
     "Context.map_proof (LocalTheory.declaration declaration)"
   #> Context.proof_map;
 
diff -r d39d64d96e71 -r e94e541346d7 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jul 28 22:01:01 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Jul 28 22:01:06 2007 +0200
@@ -6,7 +6,6 @@
 *)
 
 type local_theory = Proof.context;
-type declaration = morphism -> Context.generic -> Context.generic;
 
 signature LOCAL_THEORY =
 sig
diff -r d39d64d96e71 -r e94e541346d7 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Jul 28 22:01:01 2007 +0200
+++ b/src/Pure/morphism.ML	Sat Jul 28 22:01:06 2007 +0200
@@ -10,6 +10,7 @@
 signature BASIC_MORPHISM =
 sig
   type morphism
+  type declaration = morphism -> Context.generic -> Context.generic
   val $> : morphism * morphism -> morphism
 end
 
@@ -51,6 +52,8 @@
   term: term -> term,
   fact: thm list -> thm list};
 
+type declaration = morphism -> Context.generic -> Context.generic;
+
 fun name (Morphism {name, ...}) = name;
 fun var (Morphism {var, ...}) = var;
 fun typ (Morphism {typ, ...}) = typ;