src/HOL/Tools/ATP/atp_problem_generate.ML

                        ? add_schematic_const x
                       | _ => I)
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
 
 val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), @{sort type})
 val tvar_a = TVar tvar_a_z
 val tvar_a_name = tvar_name tvar_a_z
 val itself_name = `make_fixed_type_const @{type_name itself}
 val TYPE_name = `(make_fixed_const NONE) @{const_name Pure.type}
 val tvar_a_atype = AType ((tvar_a_name, []), [])

 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
 fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
     let
-      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
     in
       if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
       else decls
     end
   | rationalize_decls _ decls = decls