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;