# HG changeset patch
# User wenzelm
# Date 1319840638 -7200
# Node ID 255200892a421fe6817deca8ab40754d1b124b1a
# Parent  3c5d3d28605558e4d35db40e2c075c68a07bd278
tuned;

diff -r 3c5d3d286055 -r 255200892a42 src/Pure/Isar/element.ML
--- 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)]}