# HG changeset patch
# User haftmann
# Date 1401521707 -7200
# Node ID 5e9507c002cc1186577316b19f3853fd200a72fc
# Parent  7b31461802914980d480ce19cee4b3f683823f12
dropped accidental duplicate application of morphism

diff -r 7b3146180291 -r 5e9507c002cc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri May 30 18:48:05 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sat May 31 09:35:07 2014 +0200
@@ -359,7 +359,7 @@
   let
     val dangling_params' = map (Morphism.term phi) dangling_params;
     val b' = Morphism.binding phi b;
-    val b_def = Morphism.binding phi (Binding.suffix_name "_dict" b');
+    val b_def = Binding.suffix_name "_dict" b';
     val rhs' = Morphism.term phi rhs;
     val c' = Sign.full_name thy b';
     val ty' = map Term.fastype_of dangling_params' ---> Term.fastype_of rhs';