diff -r 5f2a555b15d6 -r aab49f3cf802 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:37:11 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:37:21 2011 +0200
@@ -14,7 +14,6 @@
 
   datatype type_system =
     Tags of bool |
-    Preds of bool |
     Const_Args |
     Mangled |
     No_Types
@@ -64,13 +63,11 @@
 
 datatype type_system =
   Tags of bool |
-  Preds of bool |
   Const_Args |
   Mangled |
   No_Types
 
 fun types_dangerous_types (Tags _) = true
-  | types_dangerous_types (Preds _) = true
   | types_dangerous_types _ = false
 
 (* This is an approximation. If it returns "true" for a constant that isn't
@@ -86,7 +83,6 @@
 fun needs_type_args thy type_sys s =
   case type_sys of
     Tags full_types => not full_types andalso is_overloaded thy s
-  | Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
   | Const_Args => is_overloaded thy s
   | Mangled => true
   | No_Types => false