| changeset 45289 | 25e9e7f527b4 |
| parent 43790 | 9bd8d4addd6e |
| child 45396 | 35e378c11283 |
--- a/src/Pure/variable.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/variable.ML Fri Oct 28 15:38:41 2011 +0200 @@ -456,7 +456,7 @@ val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; - in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end; + in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end;