diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/Brackin.thy
--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
-
-A couple from Steve Brackin's work.
-*)
-
-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  
-  ('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