src/Pure/Isar/class.ML
changeset 57139 5e9507c002cc
parent 57119 f6d1f88021be
child 57140 26df5a93ec27
--- 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';