replaced Nitpick's hardwired basic_ersatz_table by context data
authorkrauss
Tue Aug 02 12:27:24 2011 +0200 (2011-08-02)
changeset 4401651184010c609
parent 44015 a1507f567de6
child 44017 e828be67dfe7
replaced Nitpick's hardwired basic_ersatz_table by context data
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Nitpick.thy	Tue Aug 02 12:17:48 2011 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Aug 02 12:27:24 2011 +0200
     1.3 @@ -226,7 +226,14 @@
     1.4  use "Tools/Nitpick/nitpick_tests.ML"
     1.5  use "Tools/Nitpick/nitrox.ML"
     1.6  
     1.7 -setup {* Nitpick_Isar.setup *}
     1.8 +setup {*
     1.9 +  Nitpick_Isar.setup #>
    1.10 +  Nitpick_HOL.register_ersatz_global
    1.11 +    [(@{const_name card}, @{const_name card'}),
    1.12 +     (@{const_name setsum}, @{const_name setsum'}),
    1.13 +     (@{const_name fold_graph}, @{const_name fold_graph'}),
    1.14 +     (@{const_name wf}, @{const_name wf'})]
    1.15 +*}
    1.16  
    1.17  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.18      FunBox PairBox Word prod refl' wf' card' setsum'
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:17:48 2011 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:27:24 2011 +0200
     2.3 @@ -1868,15 +1868,8 @@
     2.4              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
     2.5            | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
     2.6  
     2.7 -(* TODO: Move to "Nitpick.thy" *)
     2.8 -val basic_ersatz_table =
     2.9 -  [(@{const_name card}, @{const_name card'}),
    2.10 -   (@{const_name setsum}, @{const_name setsum'}),
    2.11 -   (@{const_name fold_graph}, @{const_name fold_graph'}),
    2.12 -   (@{const_name wf}, @{const_name wf'})]
    2.13 -
    2.14  fun ersatz_table ctxt =
    2.15 - (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
    2.16 + #ersatz_table (Data.get (Context.Proof ctxt))
    2.17   |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt)))
    2.18  
    2.19  fun add_simps simp_table s eqs =