# HG changeset patch
# User blanchet
# Date 1410535805 -7200
# Node ID a016c42d136d0d0f3e5c3f1dc00751a85df9a7c7
# Parent  a31404ec741473c6124824eac5fb3a8e84abdb71
new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead

diff -r a31404ec7414 -r a016c42d136d src/HOL/Datatype_Examples/Brackin.thy
--- a/src/HOL/Datatype_Examples/Brackin.thy	Fri Sep 12 16:42:36 2014 +0200
+++ b/src/HOL/Datatype_Examples/Brackin.thy	Fri Sep 12 17:30:05 2014 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Datatype_Benchmark/Brackin.thy
+(*  Title:      HOL/Datatype_Examples/Brackin.thy
 
 A couple of datatypes from Steve Brackin's work.
 *)
diff -r a31404ec7414 -r a016c42d136d src/HOL/Datatype_Examples/Instructions.thy
--- a/src/HOL/Datatype_Examples/Instructions.thy	Fri Sep 12 16:42:36 2014 +0200
+++ b/src/HOL/Datatype_Examples/Instructions.thy	Fri Sep 12 17:30:05 2014 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
+(*  Title:      HOL/Datatype_Examples/Instructions.thy
 
 Example from Konrad: 68000 instruction set.
 *)
@@ -59,7 +59,7 @@
 | pcdisp nat
 | pcindex nat DataOrAddressRegister Size
 
-datatype M68kInstruction =
+old_datatype M68kInstruction =
   ABCD AddressingMode AddressingMode
 | ADD Size AddressingMode AddressingMode
 | ADDA Size AddressingMode AddressRegister
diff -r a31404ec7414 -r a016c42d136d src/HOL/Datatype_Examples/SML.thy
--- a/src/HOL/Datatype_Examples/SML.thy	Fri Sep 12 16:42:36 2014 +0200
+++ b/src/HOL/Datatype_Examples/SML.thy	Fri Sep 12 17:30:05 2014 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Datatype_Benchmark/SML.thy
+(*  Title:      HOL/Datatype_Examples/SML.thy
 
 Example from Myra: part of the syntax of SML.
 *)
@@ -32,7 +32,7 @@
 datatype
   'a long = BASE 'a | QUALIFIED strid "'a long"
 
-datatype
+old_datatype
    atpat_e = WILDCARDatpat_e
            | SCONatpat_e scon
            | VARatpat_e var
diff -r a31404ec7414 -r a016c42d136d src/HOL/Datatype_Examples/Verilog.thy
--- a/src/HOL/Datatype_Examples/Verilog.thy	Fri Sep 12 16:42:36 2014 +0200
+++ b/src/HOL/Datatype_Examples/Verilog.thy	Fri Sep 12 17:30:05 2014 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
+(*  Title:      HOL/Datatype_Examples/Verilog.thy
 
 Example from Daryl: a Verilog grammar.
 *)
 
 theory Verilog imports Main begin
 
-datatype
+old_datatype
   Source_text
      = module string "string list" "Module_item list"
      | Source_textMeta string