src/HOL/Extraction.thy

--- a/src/HOL/Extraction.thy	Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Extraction.thy	Sun Sep 14 22:59:30 2014 +0200
@@ -37,7 +37,7 @@
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_true_def induct_false_def
 
-datatype sumbool = Left | Right
+datatype (plugins only: code) sumbool = Left | Right
 
 subsection {* Type of extracted program *}