src/HOL/Tools/ATP/atp_problem_generate.ML

           else
             T_args
         end)
   end
 
-val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
-val fused_infinite_type = Type (fused_infinite_type_name, [])
-
 fun raw_atp_type_of_typ type_enc =
   let
     fun term (Type (s, Ts)) =
       AType
         ((if s = \<^type_name>\<open>fun\<close> andalso is_type_enc_higher_order type_enc then
             `I tptp_fun_type
           else if s = \<^type_name>\<open>bool\<close> andalso is_type_enc_full_higher_order type_enc then
             `I tptp_bool_type
-          else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
-            `I tptp_individual_type
           else
             `make_fixed_type_const s, []), map term Ts)
     | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
     | term (TVar z) = AType ((tvar_name z, []), [])
   in term end

         | (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy NONE s ary) j
         | _ => false)
       | _ => should_encode_type ctxt mono level T)
     end
   | should_tag_with_type _ _ _ _ _ _ = false
-
-fun fused_type ctxt mono level =
-  let
-    val should_encode = should_encode_type ctxt mono level
-    fun fuse 0 T = if should_encode T then T else fused_infinite_type
-      | fuse ary (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
-        fuse 0 T1 --> fuse (ary - 1) T2
-      | fuse _ _ = raise Fail "expected function type"
-  in fuse end
 
 (** predicators and application operators **)
 
 type sym_info =
   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,

 fun mk_aterm type_enc name T_args args =
   let val (ty_args, tm_args) = process_type_args type_enc T_args in
     ATerm ((name, ty_args), tm_args @ args)
   end
 
-fun do_bound_type ctxt mono type_enc =
+fun do_bound_type type_enc =
   (case type_enc of
-    Native (_, _, level) =>
-    fused_type ctxt mono level 0 #> native_atp_type_of_typ type_enc false 0 #> SOME
+    Native _ => native_atp_type_of_typ type_enc false 0 #> SOME
   | _ => K NONE)
 
 fun tag_with_type ctxt mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
   |> mangle_type_args_in_iterm type_enc

         ATyQuant (q, map (apfst (native_atp_type_of_typ type_enc false 0)) xs, do_formula pos phi)
       | do_formula pos (AQuant (q, xs, phi)) =
         let
           val phi = phi |> do_formula pos
           val universal = Option.map (q = AExists ? not) pos
-          val do_bound_type = do_bound_type ctxt mono type_enc
         in
           AQuant (q, xs |> map (apsnd (fn NONE => NONE
-                                        | SOME T => do_bound_type T)),
+                                        | SOME T => do_bound_type type_enc T)),
                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
                       (map_filter
                            (fn (_, NONE) => NONE
                              | (s, SOME T) =>
                                do_out_of_bound_type pos phi universal (s, T))

   (case type_enc of
     Native _ => K []
   | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
   | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
 
-fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
+fun decl_line_of_sym ctxt type_enc s (s', T_args, T, pred_sym, ary, _) =
   let
     val thy = Proof_Context.theory_of ctxt
     val (T, T_args) =
       if null T_args then
         (T, [])

             val T = s' |> robust_const_type thy
           in (T, robust_const_type_args thy (s', T)) end
         | NONE => raise Fail "unexpected type arguments")
   in
     Sym_Decl (sym_decl_prefix ^ s, (s, s'),
-              T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
-                |> native_atp_type_of_typ type_enc pred_sym ary
-                |> not (null T_args)
-                   ? curry APi (map (tvar_name o dest_TVar) T_args))
+      T |> native_atp_type_of_typ type_enc pred_sym ary
+        |> not (null T_args) ? curry APi (map (tvar_name o dest_TVar) T_args))
   end
 
 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
 
 fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j

     end
   | rationalize_decls _ decls = decls
 
 fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
   (case type_enc of
-    Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
+    Native _ => [decl_line_of_sym ctxt type_enc s (hd decls)]
   | Guards (_, level) =>
     let
       val thy = Proof_Context.theory_of ctxt
       val decls = decls |> rationalize_decls thy
       val n = length decls

           mk_app_op type_enc (list_app (do_const name1) first_bounds) last_bound
           |> filter_ty_args
         val tm2 =
           list_app (do_const name2) (first_bounds @ [last_bound])
           |> filter_ty_args
-        val do_bound_type = do_bound_type ctxt mono type_enc
         val eq =
-          eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) bounds) false
-            (atp_term_of tm1) (atp_term_of tm2)
+          eq_formula type_enc (atomic_types_of T)
+            (map (apsnd (do_bound_type type_enc)) bounds) false (atp_term_of tm1) (atp_term_of tm2)
       in
         ([tm1, tm2],
          [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
             isabelle_info generate_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I