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