Admin/Benchmarks/HOL-datatype/Brackin.thy

 (*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
     ID:         $Id$
 *)
 
-Brackin = Main +
+theory Brackin = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* A couple from Steve Brackin's work.                                       *)
 (* ------------------------------------------------------------------------- *)
 

                 X32 | X33 | X34
 
 datatype  
   ('a, 'b, 'c) TY1 =
       NoF__
-    | Fk__ 'a (('a, 'b, 'c) TY2)
+    | Fk__ 'a "('a, 'b, 'c) TY2"
 and
   ('a, 'b, 'c) TY2 =
       Ta__ bool
     | Td__ bool
-    | Tf__ (('a, 'b, 'c) TY1)
+    | 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)
+    | 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)
+    | 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)
+    | 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