# HG changeset patch
# User ballarin
# Date 1227632821 -3600
# Node ID 6f28fa3bc430b276bfe2c72ae750277ac328204b
# Parent  9cb1297b6f139446c5ef74d5941ec72e2b7a747b
Expression types cleaned up.

diff -r 9cb1297b6f13 -r 6f28fa3bc430 src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Tue Nov 25 18:06:49 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Tue Nov 25 18:07:01 2008 +0100
@@ -19,13 +19,13 @@
 val locale_val =
   Expression.parse_expression --
     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair (Expression.empty_expr, []);
+  Scan.repeat1 SpecParse.context_element >> pair ([], []);
 
 in
 
 val _ =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) ((Expression.empty_expr, []), []) -- P.opt_begin
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
             (Expression.add_locale name name expr elems #-> TheoryTarget.begin)));