# HG changeset patch
# User lcp
# Date 778842136 -7200
# Node ID 465075fd257b3856f30d198febb14aff4159394c
# Parent  909e00299009e581b95f26f88ab71bb228849a2c
removal of needless quotes

diff -r 909e00299009 -r 465075fd257b src/ZF/List.thy
--- a/src/ZF/List.thy	Wed Aug 31 17:34:12 1994 +0200
+++ b/src/ZF/List.thy	Tue Sep 06 11:02:16 1994 +0200
@@ -30,7 +30,7 @@
 
   
 datatype
-  "list(A)" = "Nil" | "Cons" ("a:A", "l: list(A)")
+  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
 
 
 translations
diff -r 909e00299009 -r 465075fd257b src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Wed Aug 31 17:34:12 1994 +0200
+++ b/src/ZF/ex/TF.thy	Tue Sep 06 11:02:16 1994 +0200
@@ -18,9 +18,9 @@
   tree, forest, tree_forest    :: "i=>i"
 
 datatype
-  "tree(A)"   = "Tcons" ("a: A",  "f: forest(A)")
+  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
 and
-  "forest(A)" = "Fnil"  |  "Fcons" ("t: tree(A)",  "f: forest(A)")
+  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
 
 rules
   TF_rec_def