diff -r a2f236a717fa -r b3ef64cadcad src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 07 11:31:41 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 07 11:32:31 2009 +0100
@@ -186,7 +186,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
+      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
   end;