# HG changeset patch
# User wenzelm
# Date 1268329970 -3600
# Node ID 68f7603f2aeb46f7ebb9f0dce85ff7fb7c379b5a
# Parent  428284ee1465909ea95630049b0c6fa34a5ec22b
actually apply morphism to binding;

diff -r 428284ee1465 -r 68f7603f2aeb src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Thu Mar 11 16:56:22 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Thu Mar 11 18:52:50 2010 +0100
@@ -39,8 +39,9 @@
         | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
     |> Local_Theory.checkpoint
     |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
-    |> Local_Theory.type_syntax false
-      (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+    |> Local_Theory.type_syntax false (fn phi =>
+        let val b' = Morphism.binding phi b
+        in Context.mapping (Sign.type_alias b' name) (ProofContext.type_alias b' name) end)
     |> ProofContext.type_alias b name
     |> Variable.declare_typ T
     |> pair T