# HG changeset patch
# User wenzelm
# Date 1365762051 -7200
# Node ID 0539e75b41704dd8be4ead2bd83e96a99eba7829
# Parent  c0af8bbc58256a2120c9c3702161bf4ea0426a55
proper identifiers -- avoid crash of case translations;

diff -r c0af8bbc5825 -r 0539e75b4170 src/HOL/Datatype_Benchmark/Brackin.thy
--- a/src/HOL/Datatype_Benchmark/Brackin.thy	Fri Apr 12 08:27:43 2013 +0200
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy	Fri Apr 12 12:20:51 2013 +0200
@@ -5,39 +5,37 @@
 
 theory Brackin imports Main begin
 
-datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
-                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
-                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
-                X32 | X33 | X34
+datatype T =
+    X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+    X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+    X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+    X32 | X33 | X34
 
-datatype  
-  ('a, 'b, 'c) TY1 =
-      NoF__
-    | Fk__ 'a "('a, 'b, 'c) TY2"
-and
-  ('a, 'b, 'c) TY2 =
-      Ta__ bool
-    | Td__ bool
-    | Tf__ "('a, 'b, 'c) TY1"
-    | Tk__ bool
-    | Tp__ bool
-    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
-    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and
-  ('a, 'b, 'c) TY3 =
-      NoS__
-    | Fresh__ "('a, 'b, 'c) TY2"
-    | Trustworthy__ 'a
-    | PrivateKey__ 'a 'b 'c
-    | PublicKey__ 'a 'b 'c
-    | Conveyed__ 'a "('a, 'b, 'c) TY2"
-    | Possesses__ 'a "('a, 'b, 'c) TY2"
-    | Received__ 'a "('a, 'b, 'c) TY2"
-    | Recognizes__ 'a "('a, 'b, 'c) TY2"
-    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
-    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
-    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
-    | Believes__ 'a "('a, 'b, 'c) TY3"
-    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+datatype ('a, 'b, 'c) TY1 =
+      NoF
+    | Fk 'a "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY2 =
+      Ta bool
+    | Td bool
+    | Tf "('a, 'b, 'c) TY1"
+    | Tk bool
+    | Tp bool
+    | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+    | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY3 =
+      NoS
+    | Fresh "('a, 'b, 'c) TY2"
+    | Trustworthy 'a
+    | PrivateKey 'a 'b 'c
+    | PublicKey 'a 'b 'c
+    | Conveyed 'a "('a, 'b, 'c) TY2"
+    | Possesses 'a "('a, 'b, 'c) TY2"
+    | Received 'a "('a, 'b, 'c) TY2"
+    | Recognizes 'a "('a, 'b, 'c) TY2"
+    | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
+    | Sends 'a "('a, 'b, 'c) TY2" 'b
+    | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
+    | Believes 'a "('a, 'b, 'c) TY3"
+    | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
 
 end