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