filter out all schematic theorems if the problem contains no ground constants

--- a/src/HOL/Tools/monomorph.ML	Sun Sep 04 21:04:02 2011 -0700
+++ b/src/HOL/Tools/monomorph.ML	Mon Sep 05 11:28:10 2011 +0200
@@ -319,7 +319,7 @@
     val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
   in
     if Symtab.is_empty known_grounds then
-      (map (single o pair 0 o snd) rthms, ctxt)
+      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
     else
       make_subst_ctxt ctxt thm_infos known_grounds subs
       |> limit_rounds ctxt (collect_substitutions thm_infos)