--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 13:50:17 2011 +0200
@@ -152,8 +152,8 @@
error ("Unknown parameter: " ^ quote name ^ "."))
-(* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are
- handled correctly. *)
+(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
+ read correctly. *)
val implode_param = strip_spaces_except_between_idents o space_implode " "
structure Data = Theory_Data