# HG changeset patch
# User blanchet
# Date 1409695585 -7200
# Node ID ca7ea280e906d42cfd49cc75b24708c2e0971610
# Parent  6fe60a9a5bad9b317e22dfe03a97913dc511feba
use 'datatype_new'

diff -r 6fe60a9a5bad -r ca7ea280e906 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Wed Sep 03 00:06:24 2014 +0200
+++ b/src/HOL/Extraction.thy	Wed Sep 03 00:06:25 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_new sumbool = Left | Right
 
 subsection {* Type of extracted program *}