diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -386,8 +386,8 @@
    prem_kind = prem_kind,
    formats = formats,
    best_slices = fn ctxt =>
-     let val (max_relevant, type_sys) = best_slice ctxt in
-       [(1.0, (false, (max_relevant, type_sys, "")))]
+     let val (max_relevant, type_enc) = best_slice ctxt in
+       [(1.0, (false, (max_relevant, type_enc, "")))]
      end}
 
 fun remotify_config system_name system_versions best_slice