# HG changeset patch
# User blanchet
# Date 1281108191 -7200
# Node ID f26d590dce0fb1e0533148ff64588ad62f2a9e88
# Parent  84205712504392791cbcb55315dd30fc74457f60
adapt occurrences of renamed Nitpick functions

diff -r 842057125043 -r f26d590dce0f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 06 17:23:11 2010 +0200
@@ -1724,7 +1724,8 @@
 *}
 
 setup {*
-Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
+Nitpick_Model.register_term_postprocessor_global @{typ "'a multiset"}
+    multiset_postproc
 *}
 
 end
diff -r 842057125043 -r f26d590dce0f src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 06 17:23:11 2010 +0200
@@ -122,14 +122,16 @@
 oops
 
 ML {*
-(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
                          - snd (HOLogic.dest_number t2))
   | my_int_postproc _ _ _ _ t = t
 *}
 
-setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
+setup {*
+Nitpick_Model.register_term_postprocessor_global @{typ my_int}
+                                                 my_int_postproc
+*}
 
 lemma "add x y = add x x"
 nitpick [show_datatypes]
@@ -212,7 +214,7 @@
 sorry
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} ""
+Nitpick_HOL.register_codatatype_global @{typ "'a llist"} ""
     (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
diff -r 842057125043 -r f26d590dce0f src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/Rat.thy	Fri Aug 06 17:23:11 2010 +0200
@@ -1174,7 +1174,7 @@
 *}
 
 setup {*
-  Nitpick.register_frac_type @{type_name rat}
+  Nitpick_HOL.register_frac_type_global @{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 842057125043 -r f26d590dce0f src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/RealDef.thy	Fri Aug 06 17:23:11 2010 +0200
@@ -1796,7 +1796,7 @@
 *}
 
 setup {*
-  Nitpick.register_frac_type @{type_name real}
+  Nitpick_HOL.register_frac_type_global @{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}),
diff -r 842057125043 -r f26d590dce0f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 17:23:11 2010 +0200
@@ -652,7 +652,7 @@
          not (is_basic_datatype thy [(NONE, true)] co_s) then
         ()
       else
-        raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
+        raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], [])
     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
                                    codatatypes
   in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end