src/Pure/Isar/class_target.ML
changeset 31697 fd841fc9ee9e
parent 31635 8623244a50d5
child 31869 01fed718958c
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed Jun 17 17:42:36 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Jun 17 17:42:41 2009 +0200
     1.3 @@ -351,7 +351,7 @@
     1.4      val c' = Sign.full_name thy b;
     1.5      val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     1.6      val ty' = Term.fastype_of rhs';
     1.7 -    val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs';
     1.8 +    val rhs'' = map_types Logic.varifyT rhs';
     1.9    in
    1.10      thy
    1.11      |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')