src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 38290 581a402a80f0
parent 38289 74dd8dd33512
child 38395 2d6dc3f25686
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 14:00:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 14:08:30 2010 +0200
@@ -535,8 +535,8 @@
 val dangerous_types = [@{type_name unit}, @{type_name bool}];
 
 (* Facts containing variables of type "unit" or "bool" or of the form
-   "!x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are
-   omitted. *)
+   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
+   are omitted. *)
 fun is_dangerous_term _ @{prop True} = true
   | is_dangerous_term full_types t =
     not full_types andalso