src/HOL/Nitpick.thy
changeset 69593 3dda49e08b9d
parent 67399 eab6ce8368fa
child 69605 a96320074298
     1.1 --- a/src/HOL/Nitpick.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -219,12 +219,12 @@
     1.4  
     1.5  setup \<open>
     1.6    Nitpick_HOL.register_ersatz_global
     1.7 -    [(@{const_name card}, @{const_name card'}),
     1.8 -     (@{const_name sum}, @{const_name sum'}),
     1.9 -     (@{const_name fold_graph}, @{const_name fold_graph'}),
    1.10 -     (@{const_name wf}, @{const_name wf'}),
    1.11 -     (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    1.12 -     (@{const_name wfrec}, @{const_name wfrec'})]
    1.13 +    [(\<^const_name>\<open>card\<close>, \<^const_name>\<open>card'\<close>),
    1.14 +     (\<^const_name>\<open>sum\<close>, \<^const_name>\<open>sum'\<close>),
    1.15 +     (\<^const_name>\<open>fold_graph\<close>, \<^const_name>\<open>fold_graph'\<close>),
    1.16 +     (\<^const_name>\<open>wf\<close>, \<^const_name>\<open>wf'\<close>),
    1.17 +     (\<^const_name>\<open>wf_wfrec\<close>, \<^const_name>\<open>wf_wfrec'\<close>),
    1.18 +     (\<^const_name>\<open>wfrec\<close>, \<^const_name>\<open>wfrec'\<close>)]
    1.19  \<close>
    1.20  
    1.21  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod