# HG changeset patch
# User immler
# Date 1528874764 -7200
# Node ID 2a2ef4552aafe8b9d41c1b81a88bf34b0837c19c
# Parent  c6a38342376eed8284d5c56f63b3ae48a5485cc0
tuned

diff -r c6a38342376e -r 2a2ef4552aaf src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:22:58 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:26:04 2018 +0200
@@ -61,6 +61,7 @@
 fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
 
 val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
-  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) "internalize a sort"))
+  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
+    "internalize and unoverload type class parameters"))
 
 end
\ No newline at end of file