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.
tuned Locale.add_thmss;
authorwenzelm
Wed, 10 Jul 2002 14:50:08 +0200
changeset 13335 7995b3f4ca5e
parent 13334 27149d72bdff
child 13336 1bd21b082466
tuned Locale.add_thmss;
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof.ML	Wed Jul 10 14:49:06 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 10 14:50:08 2002 +0200
@@ -818,12 +818,12 @@
       |> (case locale_spec of None => I | Some (loc, (loc_atts, loc_attss)) => fn thy =>
         if length names <> length loc_attss then
           raise THEORY ("Bad number of locale attributes", [thy])
-        else (locale_ctxt, thy)
+        else (thy, locale_ctxt)
           |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
-          |> (fn ((ctxt', thy'), res) =>
+          |> (fn ((thy', ctxt'), res) =>
             if name = "" andalso null loc_atts then thy'
-            else (ctxt', thy')
-              |> (#2 o #1 o Locale.add_thmss loc [((name, flat res), loc_atts)])))
+            else (thy', ctxt')
+              |> (#1 o #1 o Locale.add_thmss loc [((name, flat res), loc_atts)])))
       |> Locale.smart_have_thmss k locale_spec
         ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
       |> (fn (thy, res) => (thy, res)
isabelle