re-arranged tuples (theory * 'a) to ('a * theory) in Pure
authorhaftmann
Fri, 16 Dec 2005 15:52:05 +0100
changeset 18421 464c93701351
parent 18420 9470061ab283
child 18422 875451c9d253
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Dec 16 12:15:54 2005 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 16 15:52:05 2005 +0100
@@ -90,8 +90,8 @@
       |> (fn (_, thy) => (thy, ProofContext.init thy))
   | smart_theorems kind (SOME loc) args thy = thy
       |> Locale.note_thmss kind loc args
-      |> tap (present_theorems kind o swap o apfst #1)
-      |> #1;
+      |> tap (present_theorems kind o apsnd fst)
+      |> #2;
 
 fun declare_theorems opt_loc args =
   smart_theorems "" opt_loc [(("", []), args)];
--- a/src/Pure/Isar/locale.ML	Fri Dec 16 12:15:54 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 16 15:52:05 2005 +0100
@@ -72,13 +72,13 @@
   (* Storing results *)
   val smart_note_thmss: string -> string option ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
-    theory -> theory * (bstring * thm list) list
+    theory -> (bstring * thm list) list * theory
   val note_thmss: string -> xstring ->
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
-    theory -> (theory * ProofContext.context) * (bstring * thm list) list
+    theory -> (bstring * thm list) list * (theory * ProofContext.context)
   val note_thmss_i: string -> string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
-    theory -> (theory * ProofContext.context) * (bstring * thm list) list
+    theory -> (bstring * thm list) list * (theory * ProofContext.context)
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * Attrib.src list -> Element.context element list ->
@@ -1476,8 +1476,8 @@
   in fold activate regs thy end;
 
 
-fun smart_note_thmss kind NONE = swap oo PureThy.note_thmss_i (Drule.kind kind)
-  | smart_note_thmss kind (SOME loc) = swap oo note_thmss_qualified kind loc;
+fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
+  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
 
 
 local
@@ -1514,7 +1514,7 @@
       |> put_facts loc args'
       |> note_thmss_registrations kind loc args'
       |> note_thmss_qualified kind loc facts';
-  in ((thy', ctxt'), result) end;
+  in (result, (thy', ctxt')) end;
 
 in