diff -r fbb320d02420 -r 6dff6b1f5417 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 13:56:49 2012 +0200
@@ -380,7 +380,7 @@
 
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
 local
-  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
+  val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
   fun default c = const_prefix ^ lookup_const c
 in
   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal