author | haftmann |
Wed, 17 Jun 2009 17:42:41 +0200 | |
changeset 31697 | fd841fc9ee9e |
parent 31696 | 8b3dac635907 |
child 31698 | 9fc407df200c |
--- a/src/Pure/Isar/class_target.ML Wed Jun 17 17:42:36 2009 +0200 +++ b/src/Pure/Isar/class_target.ML Wed Jun 17 17:42:41 2009 +0200 @@ -351,7 +351,7 @@ 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'')