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