# HG changeset patch
# User wenzelm
# Date 1257190499 -3600
# Node ID 1b5ba4e6a9534af856e0cbce450a5f011c64fcc8
# Parent  12d79ece3f7eb3b0f3f7df59fab1ee8733bdd1f1
modernized structure Simple_Syntax;

diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/HOL/Library/OptionalSugar.thy
--- 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
diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/HOL/Typerep.thy
--- 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
diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/Pure/Syntax/simple_syntax.ML
--- 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 *)
diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/Pure/conjunction.ML
--- 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;
diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/Pure/drule.ML
--- 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;
 
diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/Pure/pure_thy.ML
--- 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;