make SML/NJ happy;
authorwenzelm
Sun Oct 25 13:04:06 2009 +0100 (2009-10-25)
changeset 33159369da293bbd4
parent 33156 57222d336c86
child 33160 ccbd4ad5a965
make SML/NJ happy;
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Oct 25 11:58:11 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Oct 25 13:04:06 2009 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  structure Attributes = TheoryDataFun
     1.5  (
     1.6    type T = ((src -> attribute) * string) Name_Space.table;
     1.7 -  val empty = Name_Space.empty_table "attribute";
     1.8 +  val empty : T = Name_Space.empty_table "attribute";
     1.9    val copy = I;
    1.10    val extend = I;
    1.11    fun merge _ tables : T = Name_Space.merge_tables tables;
     2.1 --- a/src/Pure/Isar/locale.ML	Sun Oct 25 11:58:11 2009 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sun Oct 25 13:04:06 2009 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  structure Locales = TheoryDataFun
     2.5  (
     2.6    type T = locale Name_Space.table;
     2.7 -  val empty = Name_Space.empty_table "locale";
     2.8 +  val empty : T = Name_Space.empty_table "locale";
     2.9    val copy = I;
    2.10    val extend = I;
    2.11    fun merge _ = Name_Space.join_tables (K merge_locale);
     3.1 --- a/src/Pure/Isar/method.ML	Sun Oct 25 11:58:11 2009 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Sun Oct 25 13:04:06 2009 +0100
     3.3 @@ -323,7 +323,7 @@
     3.4  structure Methods = TheoryDataFun
     3.5  (
     3.6    type T = ((src -> Proof.context -> method) * string) Name_Space.table;
     3.7 -  val empty = Name_Space.empty_table "method";
     3.8 +  val empty : T = Name_Space.empty_table "method";
     3.9    val copy = I;
    3.10    val extend = I;
    3.11    fun merge _ tables : T = Name_Space.merge_tables tables;
     4.1 --- a/src/Pure/simplifier.ML	Sun Oct 25 11:58:11 2009 +0100
     4.2 +++ b/src/Pure/simplifier.ML	Sun Oct 25 13:04:06 2009 +0100
     4.3 @@ -148,7 +148,7 @@
     4.4  structure Simprocs = GenericDataFun
     4.5  (
     4.6    type T = simproc Name_Space.table;
     4.7 -  val empty = Name_Space.empty_table "simproc";
     4.8 +  val empty : T = Name_Space.empty_table "simproc";
     4.9    val extend = I;
    4.10    fun merge _ simprocs = Name_Space.merge_tables simprocs;
    4.11  );
     5.1 --- a/src/Pure/theory.ML	Sun Oct 25 11:58:11 2009 +0100
     5.2 +++ b/src/Pure/theory.ML	Sun Oct 25 13:04:06 2009 +0100
     5.3 @@ -89,7 +89,7 @@
     5.4  structure ThyData = TheoryDataFun
     5.5  (
     5.6    type T = thy;
     5.7 -  val empty_axioms = Name_Space.empty_table "axiom";
     5.8 +  val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
     5.9    val empty = make_thy (empty_axioms, Defs.empty, ([], []));
    5.10    val copy = I;
    5.11  
     6.1 --- a/src/Pure/thm.ML	Sun Oct 25 11:58:11 2009 +0100
     6.2 +++ b/src/Pure/thm.ML	Sun Oct 25 13:04:06 2009 +0100
     6.3 @@ -1727,7 +1727,7 @@
     6.4  structure Oracles = TheoryDataFun
     6.5  (
     6.6    type T = unit Name_Space.table;
     6.7 -  val empty = Name_Space.empty_table "oracle";
     6.8 +  val empty : T = Name_Space.empty_table "oracle";
     6.9    val copy = I;
    6.10    val extend = I;
    6.11    fun merge _ oracles : T = Name_Space.merge_tables oracles;