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