--- 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
--- 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}])
*}
--- 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}),
--- 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}),
--- 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