| changeset 29605 | f2924219125e |
| parent 29579 | cb520b766e00 |
| child 30471 | 178de3995e91 |
--- a/src/Pure/assumption.ML Wed Jan 21 22:26:49 2009 +0100 +++ b/src/Pure/assumption.ML Wed Jan 21 22:26:49 2009 +0100 @@ -119,6 +119,6 @@ val thm = export false inner outer; val term = export_term inner outer; val typ = Logic.type_map term; - in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end; + in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end; end;