| changeset 28965 | 1de908189869 |
| parent 28625 | d51a14105e53 |
| child 29279 | 7456a64bc4f6 |
--- a/src/Pure/variable.ML Wed Dec 03 21:00:39 2008 -0800 +++ b/src/Pure/variable.ML Thu Dec 04 14:43:33 2008 +0100 @@ -398,7 +398,7 @@ val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; - in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end; + in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end;