src/Pure/CPure.thy

--- a/src/Pure/CPure.thy	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/CPure.thy	Thu Mar 27 15:32:15 2008 +0100
@@ -8,6 +8,14 @@
 imports Pure
 begin
 
-setup  -- {* Some syntax modifications, see ROOT.ML *}
+no_syntax
+  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
+  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
+
+syntax
+  "" :: "'a => cargs"  ("_")
+  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
+  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
+  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
 
 end