# HG changeset patch
# User blanchet
# Date 1410790261 -7200
# Node ID 1defb39ab329be42af7f413b28bcd5c1f2a5dd9f
# Parent  9a82544fd29f3788a962412aac9455c523a9b052
'code' is needed for extraction datatype

diff -r 9a82544fd29f -r 1defb39ab329 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Mon Sep 15 14:31:32 2014 +0200
+++ b/src/HOL/Extraction.thy	Mon Sep 15 16:11:01 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 (plugins only:) sumbool = Left | Right
+datatype (plugins only: code) sumbool = Left | Right
 
 subsection {* Type of extracted program *}