--- 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. *)