--- 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