diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -775,9 +775,6 @@
              [])
   end;
 
-val type_has_top_sort =
-  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    does, but also keep an unextensionalized version of "th" for backward
    compatibility. *)
@@ -794,6 +791,9 @@
   #> map Clausifier.introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
+val type_has_top_sort =
+  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
 fun generic_metis_tac mode ctxt ths i st0 =
   let
     val _ = trace_msg (fn () =>