src/Pure/Isar/class_target.ML

     val unchecks = these_unchecks thy [class];
     val b = Morphism.binding morph c;
     val c' = Sign.full_name thy b;
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val ty' = Term.fastype_of rhs';
-    val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs';
+    val rhs'' = map_types Logic.varifyT rhs';
   in
     thy
     |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
     |> snd
     |> Sign.add_const_constraint (c', SOME ty')