--- a/Admin/isatest/settings/at-mac-poly-5.1-para Sun Oct 25 13:18:35 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sun Oct 25 13:20:31 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly-M4 Sun Oct 25 13:18:35 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M4 Sun Oct 25 13:20:31 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -t true -q 2"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly-M8 Sun Oct 25 13:18:35 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M8 Sun Oct 25 13:20:31 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8 -t true -q 2"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly64-M4 Sun Oct 25 13:18:35 2009 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4 Sun Oct 25 13:20:31 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -q 2 -t true"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 2"
--- a/Admin/isatest/settings/mac-poly64-M8 Sun Oct 25 13:18:35 2009 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Sun Oct 25 13:20:31 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8 -q 2 -t true"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 2"
--- a/src/Pure/Isar/attrib.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Oct 25 13:20:31 2009 +0100
@@ -68,7 +68,7 @@
structure Attributes = TheoryDataFun
(
type T = ((src -> attribute) * string) Name_Space.table;
- val empty = Name_Space.empty_table "attribute";
+ val empty : T = Name_Space.empty_table "attribute";
val copy = I;
val extend = I;
fun merge _ tables : T = Name_Space.merge_tables tables;
--- a/src/Pure/Isar/locale.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Oct 25 13:20:31 2009 +0100
@@ -125,7 +125,7 @@
structure Locales = TheoryDataFun
(
type T = locale Name_Space.table;
- val empty = Name_Space.empty_table "locale";
+ val empty : T = Name_Space.empty_table "locale";
val copy = I;
val extend = I;
fun merge _ = Name_Space.join_tables (K merge_locale);
--- a/src/Pure/Isar/method.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/Isar/method.ML Sun Oct 25 13:20:31 2009 +0100
@@ -323,7 +323,7 @@
structure Methods = TheoryDataFun
(
type T = ((src -> Proof.context -> method) * string) Name_Space.table;
- val empty = Name_Space.empty_table "method";
+ val empty : T = Name_Space.empty_table "method";
val copy = I;
val extend = I;
fun merge _ tables : T = Name_Space.merge_tables tables;
--- a/src/Pure/simplifier.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/simplifier.ML Sun Oct 25 13:20:31 2009 +0100
@@ -148,7 +148,7 @@
structure Simprocs = GenericDataFun
(
type T = simproc Name_Space.table;
- val empty = Name_Space.empty_table "simproc";
+ val empty : T = Name_Space.empty_table "simproc";
val extend = I;
fun merge _ simprocs = Name_Space.merge_tables simprocs;
);
--- a/src/Pure/theory.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/theory.ML Sun Oct 25 13:20:31 2009 +0100
@@ -89,7 +89,7 @@
structure ThyData = TheoryDataFun
(
type T = thy;
- val empty_axioms = Name_Space.empty_table "axiom";
+ val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
val empty = make_thy (empty_axioms, Defs.empty, ([], []));
val copy = I;
--- a/src/Pure/thm.ML Sun Oct 25 13:18:35 2009 +0100
+++ b/src/Pure/thm.ML Sun Oct 25 13:20:31 2009 +0100
@@ -1727,7 +1727,7 @@
structure Oracles = TheoryDataFun
(
type T = unit Name_Space.table;
- val empty = Name_Space.empty_table "oracle";
+ val empty : T = Name_Space.empty_table "oracle";
val copy = I;
val extend = I;
fun merge _ oracles : T = Name_Space.merge_tables oracles;