# HG changeset patch
# User wenzelm
# Date 1211122996 -7200
# Node ID 1309a6a0a29f1b3a89189f37c0c510b4076e6526
# Parent  ebbaa935eae06249b50dfcff6769ea5888e1c53b
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

diff -r ebbaa935eae0 -r 1309a6a0a29f src/CTT/CTT.thy
--- 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
diff -r ebbaa935eae0 -r 1309a6a0a29f src/Cube/Cube.thy
--- 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
diff -r ebbaa935eae0 -r 1309a6a0a29f src/FOL/IFOL.thy
--- 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"
diff -r ebbaa935eae0 -r 1309a6a0a29f src/FOLP/IFOLP.thy
--- 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"
diff -r ebbaa935eae0 -r 1309a6a0a29f src/Sequents/Sequents.thy
--- 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