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