# HG changeset patch
# User wenzelm
# Date 1559591274 -7200
# Node ID e49bf4ebf3305211b755c00105f674dbcf090a68
# Parent  c82f59c47aafafa4c1ccaa67d340da1d40c86b09
more structural integrity;

diff -r c82f59c47aaf -r e49bf4ebf330 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Jun 03 20:09:43 2019 +0200
+++ b/src/Pure/variable.ML	Mon Jun 03 21:47:54 2019 +0200
@@ -565,6 +565,8 @@
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
   in
+    Morphism.transfer_morphism' inner $>
+    Morphism.transfer_morphism' outer $>
     Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
   end;