locale expression import;
authorwenzelm
Thu, 22 Nov 2001 23:44:57 +0100
changeset 12271 37b9c807b461
parent 12270 71534648d5d4
child 12272 9bc50336dab6
locale expression import;
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