| changeset 29605 | f2924219125e |
| parent 29279 | 7456a64bc4f6 |
| child 30756 | 1a9f93c1ed22 |
--- a/src/Pure/variable.ML Wed Jan 21 22:26:49 2009 +0100 +++ b/src/Pure/variable.ML Wed Jan 21 22:26:49 2009 +0100 @@ -397,7 +397,7 @@ val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; - in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end; + in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end;