author | haftmann |
Sat, 31 May 2014 09:35:07 +0200 | |
changeset 57139 | 5e9507c002cc |
parent 57138 | 7b3146180291 |
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';