--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 15 11:59:18 2014 +0100
@@ -2000,7 +2000,7 @@
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
- | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
+ | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
fun ersatz_table ctxt =
#ersatz_table (Data.get (Context.Proof ctxt))