# HG changeset patch
# User blanchet
# Date 1314782093 -7200
# Node ID 1e2d5cdef3d0887de11743e56624a38713e9811d
# Parent  779f79ed0ddc9e8a3da8774054b94076d0e79791
tuning

diff -r 779f79ed0ddc -r 1e2d5cdef3d0 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:12:27 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:14:53 2011 +0200
@@ -365,12 +365,6 @@
 
 (** Definitions and functions for FOL clauses and formulas for TPTP **)
 
-(* The first component is the type class; the second is a "TVar" or "TFree". *)
-datatype type_literal =
-  TyLitVar of name * name |
-  TyLitFree of name * name
-
-
 (** Isabelle arities **)
 
 datatype arity_literal =
@@ -732,10 +726,10 @@
     #> (if s = the_single @{sort HOL.type} then
           I
         else if i = ~1 then
-          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
+          insert (op =) (`make_type_class s, `make_fixed_type_var x)
         else
-          insert (op =) (TyLitVar (`make_type_class s,
-                                   (make_schematic_type_var (x, i), x))))
+          insert (op =) (`make_type_class s,
+                         (make_schematic_type_var (x, i), x)))
 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   | add_sorts_on_tfree _ = I
 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
@@ -1470,12 +1464,8 @@
     else ATerm (class, [arg, ATerm (TYPE_name, [arg])])
   | _ => ATerm (class, [arg])
 
-fun fo_literal_from_type_literal type_enc (TyLitVar (class, name)) =
-    (true, type_class_aterm type_enc class (ATerm (name, [])))
-  | fo_literal_from_type_literal type_enc (TyLitFree (class, name)) =
-    (true, type_class_aterm type_enc class (ATerm (name, [])))
-(* FIXME: Really "true" in both cases? If so, merge "TyLitVar" and
-   "TyLitFree". *)
+fun fo_literal_from_type_literal type_enc (class, name) =
+  (true, type_class_aterm type_enc class (ATerm (name, [])))
 
 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot