tuned;

--- a/src/Pure/Isar/element.ML	Fri Oct 28 23:41:16 2011 +0200
+++ b/src/Pure/Isar/element.ML	Sat Oct 29 00:23:58 2011 +0200
@@ -397,7 +397,7 @@
 fun instT_morphism thy env =
   let val thy_ref = Theory.check_thy thy in
     Morphism.morphism
-     {binding = [I],
+     {binding = [],
       typ = [instT_type env],
       term = [instT_term env],
       fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]}