src/Pure/Isar/proof_context.ML

     val arg' = (c', rhs');
   in
     Context.mapping_result
       (Sign.add_abbrev Syntax.internalM arg') (add_abbrev Syntax.internalM arg')
     #-> (fn (lhs, _) =>
-      Term.equiv_types (rhs, rhs') ? target_notation prmode [(lhs, mx)] Morphism.identity)
+      Term.equiv_types (rhs, rhs') ? Morphism.form (target_notation prmode [(lhs, mx)]))
   end;
 
 fun local_abbrev (x, rhs) =
   Variable.add_fixes [x] #-> (fn [x'] =>
     let