| changeset 45289 | 25e9e7f527b4 |
| parent 41552 | c5e71fee3617 |
| child 45650 | d314a4e8038f |
--- a/src/Pure/assumption.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/assumption.ML Fri Oct 28 15:38:41 2011 +0200 @@ -124,6 +124,6 @@ val thm = export false inner outer; val term = export_term inner outer; val typ = Logic.type_map term; - in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end; + in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end; end;