modernized structure Simple_Syntax;

--- a/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 20:34:59 2009 +0100
@@ -50,7 +50,7 @@
 (* type constraints with spacing *)
 setup {*
 let
-  val typ = SimpleSyntax.read_typ;
+  val typ = Simple_Syntax.read_typ;
   val typeT = Syntax.typeT;
   val spropT = Syntax.spropT;
 in

--- a/src/HOL/Typerep.thy	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/HOL/Typerep.thy	Mon Nov 02 20:34:59 2009 +0100
@@ -29,7 +29,7 @@
     | typerep_tr' _ T ts = raise Match;
 in
   Sign.add_syntax_i
-    [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
+    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
   #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
   #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
 end

--- a/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 20:34:59 2009 +0100
@@ -11,7 +11,7 @@
   val read_prop: string -> term
 end;
 
-structure SimpleSyntax: SIMPLE_SYNTAX =
+structure Simple_Syntax: SIMPLE_SYNTAX =
 struct
 
 (* scanning tokens *)

--- a/src/Pure/conjunction.ML	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/Pure/conjunction.ML	Mon Nov 02 20:34:59 2009 +0100
@@ -30,7 +30,7 @@
 (** abstract syntax **)
 
 fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
 
 val true_prop = certify Logic.true_prop;
 val conjunction = certify Logic.conjunction;

--- a/src/Pure/drule.ML	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/Pure/drule.ML	Mon Nov 02 20:34:59 2009 +0100
@@ -450,7 +450,7 @@
 
 (*** Meta-Rewriting Rules ***)
 
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
 
 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 

--- a/src/Pure/pure_thy.ML	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 02 20:34:59 2009 +0100
@@ -227,8 +227,8 @@
 
 (*** Pure theory syntax and logical content ***)
 
-val typ = SimpleSyntax.read_typ;
-val prop = SimpleSyntax.read_prop;
+val typ = Simple_Syntax.read_typ;
+val prop = Simple_Syntax.read_prop;
 
 val typeT = Syntax.typeT;
 val spropT = Syntax.spropT;