| changeset 54740 | 91f54d386680 |
| parent 50201 | c26369c9eda6 |
| child 55014 | a93f496f6c30 |
--- a/src/Pure/variable.ML Fri Dec 13 14:58:47 2013 +0100 +++ b/src/Pure/variable.ML Fri Dec 13 20:20:15 2013 +0100 @@ -461,7 +461,9 @@ val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; - in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end; + in + Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} + end;