modernized structure Simple_Syntax;
authorwenzelm
Mon Nov 02 20:34:59 2009 +0100 (2009-11-02)
changeset 333841b5ba4e6a953
parent 33383 12d79ece3f7e
child 33385 fb2358edcfb6
modernized structure Simple_Syntax;
src/HOL/Library/OptionalSugar.thy
src/HOL/Typerep.thy
src/Pure/Syntax/simple_syntax.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 20:30:40 2009 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 20:34:59 2009 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  (* type constraints with spacing *)
     1.5  setup {*
     1.6  let
     1.7 -  val typ = SimpleSyntax.read_typ;
     1.8 +  val typ = Simple_Syntax.read_typ;
     1.9    val typeT = Syntax.typeT;
    1.10    val spropT = Syntax.spropT;
    1.11  in
     2.1 --- a/src/HOL/Typerep.thy	Mon Nov 02 20:30:40 2009 +0100
     2.2 +++ b/src/HOL/Typerep.thy	Mon Nov 02 20:34:59 2009 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4      | typerep_tr' _ T ts = raise Match;
     2.5  in
     2.6    Sign.add_syntax_i
     2.7 -    [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
     2.8 +    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
     2.9    #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
    2.10    #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
    2.11  end
     3.1 --- a/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 20:30:40 2009 +0100
     3.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 20:34:59 2009 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4    val read_prop: string -> term
     3.5  end;
     3.6  
     3.7 -structure SimpleSyntax: SIMPLE_SYNTAX =
     3.8 +structure Simple_Syntax: SIMPLE_SYNTAX =
     3.9  struct
    3.10  
    3.11  (* scanning tokens *)
     4.1 --- a/src/Pure/conjunction.ML	Mon Nov 02 20:30:40 2009 +0100
     4.2 +++ b/src/Pure/conjunction.ML	Mon Nov 02 20:34:59 2009 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4  (** abstract syntax **)
     4.5  
     4.6  fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
     4.7 -val read_prop = certify o SimpleSyntax.read_prop;
     4.8 +val read_prop = certify o Simple_Syntax.read_prop;
     4.9  
    4.10  val true_prop = certify Logic.true_prop;
    4.11  val conjunction = certify Logic.conjunction;
     5.1 --- a/src/Pure/drule.ML	Mon Nov 02 20:30:40 2009 +0100
     5.2 +++ b/src/Pure/drule.ML	Mon Nov 02 20:34:59 2009 +0100
     5.3 @@ -450,7 +450,7 @@
     5.4  
     5.5  (*** Meta-Rewriting Rules ***)
     5.6  
     5.7 -val read_prop = certify o SimpleSyntax.read_prop;
     5.8 +val read_prop = certify o Simple_Syntax.read_prop;
     5.9  
    5.10  fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
    5.11  
     6.1 --- a/src/Pure/pure_thy.ML	Mon Nov 02 20:30:40 2009 +0100
     6.2 +++ b/src/Pure/pure_thy.ML	Mon Nov 02 20:34:59 2009 +0100
     6.3 @@ -227,8 +227,8 @@
     6.4  
     6.5  (*** Pure theory syntax and logical content ***)
     6.6  
     6.7 -val typ = SimpleSyntax.read_typ;
     6.8 -val prop = SimpleSyntax.read_prop;
     6.9 +val typ = Simple_Syntax.read_typ;
    6.10 +val prop = Simple_Syntax.read_prop;
    6.11  
    6.12  val typeT = Syntax.typeT;
    6.13  val spropT = Syntax.spropT;