diff -r 8e585c7d418a -r f8292d3020db src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Sep 14 19:38:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Sep 14 19:38:44 2010 +0200
@@ -144,7 +144,7 @@
                      |> Clausifier.introduce_combinators_in_cterm
                      |> prop_of |> Logic.dest_equals |> snd
                      |> reveal_bounds Ts
-        val ([t], ctxt') = Variable.import_terms true [t] ctxt
+        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
       handle THM _ =>
              (* A type variable of sort "{}" will make abstraction fail. *)