# HG changeset patch
# User wenzelm
# Date 1006469097 -3600
# Node ID 37b9c807b461aa0bff6605fbc93bc2051ef56128
# Parent  71534648d5d4b91940064fc1e91a4c796834928d
locale expression import;

diff -r 71534648d5d4 -r 37b9c807b461 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Nov 22 23:44:30 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Nov 22 23:44:57 2001 +0100
@@ -188,7 +188,7 @@
   val token_translation: string * Comment.text -> theory -> theory
   val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
   val add_oracle: (bstring * string) * Comment.text -> theory -> theory
-  val add_locale: bstring * xstring list * (Args.src Locale.element * Comment.text) list
+  val add_locale: bstring * Locale.expr * (Args.src Locale.element * Comment.text) list
     -> theory -> theory
   val begin_theory: string -> string list -> (string * bool) list -> theory
   val end_theory: theory -> theory