# HG changeset patch
# User krauss
# Date 1312280844 -7200
# Node ID 51184010c60953e121d4d5b795ef7b7489e16ec2
# Parent  a1507f567de6b10a360f7fc4ccad8c20837b7ba5
replaced Nitpick's hardwired basic_ersatz_table by context data

diff -r a1507f567de6 -r 51184010c609 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Aug 02 12:17:48 2011 +0200
+++ b/src/HOL/Nitpick.thy	Tue Aug 02 12:27:24 2011 +0200
@@ -226,7 +226,14 @@
 use "Tools/Nitpick/nitpick_tests.ML"
 use "Tools/Nitpick/nitrox.ML"
 
-setup {* Nitpick_Isar.setup *}
+setup {*
+  Nitpick_Isar.setup #>
+  Nitpick_HOL.register_ersatz_global
+    [(@{const_name card}, @{const_name card'}),
+     (@{const_name setsum}, @{const_name setsum'}),
+     (@{const_name fold_graph}, @{const_name fold_graph'}),
+     (@{const_name wf}, @{const_name wf'})]
+*}
 
 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
     FunBox PairBox Word prod refl' wf' card' setsum'
diff -r a1507f567de6 -r 51184010c609 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:17:48 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:27:24 2011 +0200
@@ -1868,15 +1868,8 @@
             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
 
-(* TODO: Move to "Nitpick.thy" *)
-val basic_ersatz_table =
-  [(@{const_name card}, @{const_name card'}),
-   (@{const_name setsum}, @{const_name setsum'}),
-   (@{const_name fold_graph}, @{const_name fold_graph'}),
-   (@{const_name wf}, @{const_name wf'})]
-
 fun ersatz_table ctxt =
- (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
+ #ersatz_table (Data.get (Context.Proof ctxt))
  |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt)))
 
 fun add_simps simp_table s eqs =