src/HOL/Tools/ATP/atp_translate.ML

   val polymorphism_of_type_sys : type_sys -> polymorphism
   val level_of_type_sys : type_sys -> type_level
   val is_type_sys_virtually_sound : type_sys -> bool
   val is_type_sys_fairly_sound : type_sys -> bool
   val choose_format : format list -> type_sys -> format * type_sys
-  val raw_type_literals_for_types : typ list -> type_literal list
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const_name : string -> string
   val unmangled_const : string -> string * string fo_term list
   val helper_table : ((string * bool) * thm list) list

 
 open ATP_Util
 open ATP_Problem
 
 type name = string * string
-
-(* FIXME: avoid *)
-fun union_all xss = fold (union (op =)) xss []
 
 (* experimental *)
 val generate_useful_info = false
 
 fun useful_isabelle_info s =

   TVarLit of name * name
 
 fun gen_TVars 0 = []
   | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
 
-fun pack_sort (_,[])  = []
-  | pack_sort (tvar, "HOL.type" :: srt) =
-    pack_sort (tvar, srt) (* IGNORE sort "type" *)
-  | pack_sort (tvar, cls :: srt) =
-    (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
+val type_class = the_single @{sort type}
+
+fun add_packed_sort tvar =
+  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
 
 type arity_clause =
   {name: string,
    prem_lits: arity_literal list,
    concl_lits: arity_literal}

   let
     val tvars = gen_TVars (length args)
     val tvars_srts = ListPair.zip (tvars, args)
   in
     {name = name,
-     prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
+     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
      concl_lits = TConsLit (`make_type_class cls,
                             `make_fixed_type_const tcons,
                             tvars ~~ tvars)}
   end
 

   in map try_classes tycons end
 
 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
 fun iter_type_class_pairs _ _ [] = ([], [])
   | iter_type_class_pairs thy tycons classes =
-      let val cpairs = type_class_pairs thy tycons classes
-          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
-            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
-          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
+      let
+        fun maybe_insert_class s =
+          (s <> type_class andalso not (member (op =) classes s))
+          ? insert (op =) s
+        val cpairs = type_class_pairs thy tycons classes
+        val newclasses =
+          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
+        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
       in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
 
 fun make_arity_clauses thy tycons =
   iter_type_class_pairs thy tycons ##> multi_arity_clause
 

     Explicit_Type_Args false
   else
     general_type_arg_policy type_sys
 
 (*Make literals for sorted type variables*)
-fun generic_sorts_on_type (_, []) = []
-  | generic_sorts_on_type ((x, i), s :: ss) =
-    generic_sorts_on_type ((x, i), ss)
-    |> (if s = the_single @{sort HOL.type} then
+fun generic_add_sorts_on_type (_, []) = I
+  | generic_add_sorts_on_type ((x, i), s :: ss) =
+    generic_add_sorts_on_type ((x, i), ss)
+    #> (if s = the_single @{sort HOL.type} then
           I
         else if i = ~1 then
-          cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
+          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
         else
-          cons (TyLitVar (`make_type_class s,
-                          (make_schematic_type_var (x, i), x))))
-fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
-  | sorts_on_tfree _ = []
-fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
-  | sorts_on_tvar _ = []
-
-(* Given a list of sorted type variables, return a list of type literals. *)
-fun raw_type_literals_for_types Ts =
-  union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
-
-fun type_literals_for_types type_sys sorts_on_typ Ts =
-  if level_of_type_sys type_sys = No_Types then []
-  else union_all (map sorts_on_typ Ts)
+          insert (op =) (TyLitVar (`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
+  | add_sorts_on_tvar _ = I
+
+fun type_literals_for_types type_sys add_sorts_on_typ Ts =
+  [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
 
 fun mk_aconns c phis =
   let val (phis', phi') = split_last phis in
     fold_rev (mk_aconn c) phis' phi'
   end

       | do_formula _ (AAtom tm) = AAtom (do_term tm)
   in do_formula o SOME end
 
 fun bound_tvars type_sys Ts =
   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
-                (type_literals_for_types type_sys sorts_on_tvar Ts))
+                (type_literals_for_types type_sys add_sorts_on_tvar Ts))
 
 fun formula_for_fact ctxt format nonmono_Ts type_sys
                      ({combformula, atomic_types, ...} : translated_formula) =
   combformula
   |> close_combformula_universally

                (close_combformula_universally combformula)
            |> bound_tvars type_sys atomic_types
            |> close_formula_universally, NONE, NONE)
 
 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
-  atomic_types |> type_literals_for_types type_sys sorts_on_tfree
+  atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
                |> map fo_literal_from_type_literal
 
 fun formula_line_for_free_type j lit =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
            formula_from_fo_literal lit, NONE, NONE)