# HG changeset patch
# User blanchet
# Date 1281351196 -7200
# Node ID 796302ca361176e2e5eb358fd722864c08d4c556
# Parent  c9c7bd8368942a53611dda9a3dd3399805c935c6
replace "setup" with "declaration"

diff -r c9c7bd836894 -r 796302ca3611 src/HOL/Library/Multiset.thy
--- 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
 *}
 
diff -r c9c7bd836894 -r 796302ca3611 src/HOL/Rat.thy
--- 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}),
diff -r c9c7bd836894 -r 796302ca3611 src/HOL/RealDef.thy
--- 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}),