Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed locale predicate name convention
authorhaftmann
Wed, 07 Jan 2009 22:31:34 +0100
changeset 29390 5c26e3a63b8e
parent 29379 f65670092259
child 29391 1f6e8c00dc3e
changed locale predicate name convention
src/HOL/Statespace/state_space.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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;
 
--- 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"
isabelle