# HG changeset patch
# User haftmann
# Date 1245253361 -7200
# Node ID fd841fc9ee9ed5f49a252a740c32cbd5d15d98fc
# Parent  8b3dac635907302ee9a587ae3fb794cb282de517
stripped dead comment

diff -r 8b3dac635907 -r fd841fc9ee9e src/Pure/Isar/class_target.ML
--- 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'')