# HG changeset patch
# User boehmes
# Date 1315214890 -7200
# Node ID c9cf0780cd4f63e1b633821550a8bb70b18c56b7
# Parent  d37afb90c23ef50992b7e788d1c5486295ed52a7
filter out all schematic theorems if the problem contains no ground constants

diff -r d37afb90c23e -r c9cf0780cd4f src/HOL/Tools/monomorph.ML
--- 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)