# HG changeset patch
# User blanchet
# Date 1301992641 -7200
# Node ID aab49f3cf80224634c931619cfd1d038eec22be0
# Parent  5f2a555b15d69ff2639539b9a731b45450995c7e
killed unimplemented type encoding "preds"

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
diff -r 5f2a555b15d6 -r aab49f3cf802 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 05 10:37:11 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 05 10:37:21 2011 +0200
@@ -240,7 +240,6 @@
     val type_sys =
       case (lookup_string "type_sys", lookup_bool "full_types") of
         ("tags", full_types) => Tags full_types
-      | ("preds", full_types) => Preds full_types
       | ("const_args", false) => Const_Args
       | ("mangled", false) => if monomorphize then Mangled else Const_Args
       | ("none", false) => No_Types