filter out all schematic theorems if the problem contains no ground constants
authorboehmes
Mon Sep 05 11:28:10 2011 +0200 (2011-09-05)
changeset 44717c9cf0780cd4f
parent 44716 d37afb90c23e
child 44718 b656af4c9796
filter out all schematic theorems if the problem contains no ground constants
src/HOL/Tools/monomorph.ML
     1.1 --- a/src/HOL/Tools/monomorph.ML	Sun Sep 04 21:04:02 2011 -0700
     1.2 +++ b/src/HOL/Tools/monomorph.ML	Mon Sep 05 11:28:10 2011 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4      val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
     1.5    in
     1.6      if Symtab.is_empty known_grounds then
     1.7 -      (map (single o pair 0 o snd) rthms, ctxt)
     1.8 +      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
     1.9      else
    1.10        make_subst_ctxt ctxt thm_infos known_grounds subs
    1.11        |> limit_rounds ctxt (collect_substitutions thm_infos)