--- a/src/Pure/Isar/local_theory.ML Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/local_theory.ML Fri Dec 13 20:20:15 2013 +0100
@@ -189,7 +189,8 @@
fun standard_morphism lthy ctxt =
Proof_Context.norm_export_morphism lthy ctxt $>
- Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+ Morphism.binding_morphism "Local_Theory.standard_binding"
+ (Name_Space.transform_binding (naming_of lthy));
fun standard_form lthy ctxt x =
Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);