more structural integrity;

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