re-arranged tuples (theory * 'a) to ('a * theory) in Pure
authorhaftmann
Fri Dec 16 15:52:05 2005 +0100 (2005-12-16)
changeset 18421464c93701351
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
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Dec 16 12:15:54 2005 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 16 15:52:05 2005 +0100
     1.3 @@ -90,8 +90,8 @@
     1.4        |> (fn (_, thy) => (thy, ProofContext.init thy))
     1.5    | smart_theorems kind (SOME loc) args thy = thy
     1.6        |> Locale.note_thmss kind loc args
     1.7 -      |> tap (present_theorems kind o swap o apfst #1)
     1.8 -      |> #1;
     1.9 +      |> tap (present_theorems kind o apsnd fst)
    1.10 +      |> #2;
    1.11  
    1.12  fun declare_theorems opt_loc args =
    1.13    smart_theorems "" opt_loc [(("", []), args)];
     2.1 --- a/src/Pure/Isar/locale.ML	Fri Dec 16 12:15:54 2005 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 16 15:52:05 2005 +0100
     2.3 @@ -72,13 +72,13 @@
     2.4    (* Storing results *)
     2.5    val smart_note_thmss: string -> string option ->
     2.6      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     2.7 -    theory -> theory * (bstring * thm list) list
     2.8 +    theory -> (bstring * thm list) list * theory
     2.9    val note_thmss: string -> xstring ->
    2.10      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    2.11 -    theory -> (theory * ProofContext.context) * (bstring * thm list) list
    2.12 +    theory -> (bstring * thm list) list * (theory * ProofContext.context)
    2.13    val note_thmss_i: string -> string ->
    2.14      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    2.15 -    theory -> (theory * ProofContext.context) * (bstring * thm list) list
    2.16 +    theory -> (bstring * thm list) list * (theory * ProofContext.context)
    2.17  
    2.18    val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
    2.19      string * Attrib.src list -> Element.context element list ->
    2.20 @@ -1476,8 +1476,8 @@
    2.21    in fold activate regs thy end;
    2.22  
    2.23  
    2.24 -fun smart_note_thmss kind NONE = swap oo PureThy.note_thmss_i (Drule.kind kind)
    2.25 -  | smart_note_thmss kind (SOME loc) = swap oo note_thmss_qualified kind loc;
    2.26 +fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
    2.27 +  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
    2.28  
    2.29  
    2.30  local
    2.31 @@ -1514,7 +1514,7 @@
    2.32        |> put_facts loc args'
    2.33        |> note_thmss_registrations kind loc args'
    2.34        |> note_thmss_qualified kind loc facts';
    2.35 -  in ((thy', ctxt'), result) end;
    2.36 +  in (result, (thy', ctxt')) end;
    2.37  
    2.38  in
    2.39