--- a/src/HOL/Nitpick.thy Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Nitpick.thy Mon Sep 15 10:49:07 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
-datatype (plugins only: code) (dead 'a) word = Word "'a set"
+datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype (plugins only:) (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit