--- a/src/HOL/Library/Multiset.thy Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 09 12:53:16 2010 +0200
@@ -1723,8 +1723,8 @@
| multiset_postproc _ _ _ _ t = t
*}
-setup {*
-Nitpick_Model.register_term_postprocessor_global @{typ "'a multiset"}
+declaration {*
+Nitpick_Model.register_term_postprocessor @{typ "'a multiset"}
multiset_postproc
*}
--- a/src/HOL/Rat.thy Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/Rat.thy Mon Aug 09 12:53:16 2010 +0200
@@ -1173,8 +1173,8 @@
fun rat_of_int i = (i, 1);
*}
-setup {*
- Nitpick_HOL.register_frac_type_global @{type_name rat}
+declaration {*
+ Nitpick_HOL.register_frac_type @{type_name rat}
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
(@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
(@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
--- a/src/HOL/RealDef.thy Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Aug 09 12:53:16 2010 +0200
@@ -1795,8 +1795,8 @@
fun real_of_int i = (i, 1);
*}
-setup {*
- Nitpick_HOL.register_frac_type_global @{type_name real}
+declaration {*
+ Nitpick_HOL.register_frac_type @{type_name real}
[(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
(@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
(@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),