setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

--- a/src/CTT/CTT.thy	Sun May 18 17:03:14 2008 +0200
+++ b/src/CTT/CTT.thy	Sun May 18 17:03:16 2008 +0200
@@ -11,6 +11,8 @@
 uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
 begin
 
+setup PureThy.old_appl_syntax_setup
+
 typedecl i
 typedecl t
 typedecl o

--- a/src/Cube/Cube.thy	Sun May 18 17:03:14 2008 +0200
+++ b/src/Cube/Cube.thy	Sun May 18 17:03:16 2008 +0200
@@ -9,6 +9,8 @@
 imports Pure
 begin
 
+setup PureThy.old_appl_syntax_setup
+
 typedecl "term"
 typedecl "context"
 typedecl typing

--- a/src/FOL/IFOL.thy	Sun May 18 17:03:14 2008 +0200
+++ b/src/FOL/IFOL.thy	Sun May 18 17:03:16 2008 +0200
@@ -26,6 +26,8 @@
 
 subsection {* Syntax and axiomatic basis *}
 
+setup PureThy.old_appl_syntax_setup
+
 global
 
 classes "term"

--- a/src/FOLP/IFOLP.thy	Sun May 18 17:03:14 2008 +0200
+++ b/src/FOLP/IFOLP.thy	Sun May 18 17:03:16 2008 +0200
@@ -11,6 +11,8 @@
 uses ("hypsubst.ML") ("intprover.ML")
 begin
 
+setup PureThy.old_appl_syntax_setup
+
 global
 
 classes "term"

--- a/src/Sequents/Sequents.thy	Sun May 18 17:03:14 2008 +0200
+++ b/src/Sequents/Sequents.thy	Sun May 18 17:03:16 2008 +0200
@@ -11,6 +11,8 @@
 uses ("prover.ML")
 begin
 
+setup PureThy.old_appl_syntax_setup
+
 declare [[unify_trace_bound = 20, unify_search_bound = 40]]
 
 global