Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
actually apply morphism to binding;
authorwenzelm
Thu, 11 Mar 2010 18:52:50 +0100
changeset 35714 68f7603f2aeb
parent 35713 428284ee1465
child 35715 9dc39bad4f4d
actually apply morphism to binding;
src/Pure/Isar/typedecl.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle