# HG changeset patch
# User haftmann
# Date 1231363894 -3600
# Node ID 5c26e3a63b8e8c38e21b4e8e664890f0610edb32
# Parent  f65670092259507bca6cf6da916e554c366e0dac
changed locale predicate name convention

diff -r f65670092259 -r 5c26e3a63b8e src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Jan 07 08:04:12 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Wed Jan 07 22:31:34 2009 +0100
@@ -160,7 +160,7 @@
 
 fun add_locale_cmd name expr elems thy =
   thy 
-  |> Expression.add_locale_cmd name name expr elems
+  |> Expression.add_locale_cmd name "" expr elems
   |> snd
   |> LocalTheory.exit;
 
diff -r f65670092259 -r 5c26e3a63b8e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 07 08:04:12 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 07 22:31:34 2009 +0100
@@ -393,7 +393,7 @@
     (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_cmd name name expr elems #> snd)));
+            (Expression.add_locale_cmd name "" expr elems #> snd)));
 
 val _ =
   OuterSyntax.command "sublocale"