src/Pure/Isar/locale.ML
changeset 18421 464c93701351
parent 18377 0e1d025d57b3
child 18450 e57731ba01dd
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Dec 16 12:15:54 2005 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 16 15:52:05 2005 +0100
     1.3 @@ -72,13 +72,13 @@
     1.4    (* Storing results *)
     1.5    val smart_note_thmss: string -> string option ->
     1.6      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     1.7 -    theory -> theory * (bstring * thm list) list
     1.8 +    theory -> (bstring * thm list) list * theory
     1.9    val note_thmss: string -> xstring ->
    1.10      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    1.11 -    theory -> (theory * ProofContext.context) * (bstring * thm list) list
    1.12 +    theory -> (bstring * thm list) list * (theory * ProofContext.context)
    1.13    val note_thmss_i: string -> string ->
    1.14      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.15 -    theory -> (theory * ProofContext.context) * (bstring * thm list) list
    1.16 +    theory -> (bstring * thm list) list * (theory * ProofContext.context)
    1.17  
    1.18    val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
    1.19      string * Attrib.src list -> Element.context element list ->
    1.20 @@ -1476,8 +1476,8 @@
    1.21    in fold activate regs thy end;
    1.22  
    1.23  
    1.24 -fun smart_note_thmss kind NONE = swap oo PureThy.note_thmss_i (Drule.kind kind)
    1.25 -  | smart_note_thmss kind (SOME loc) = swap oo note_thmss_qualified kind loc;
    1.26 +fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
    1.27 +  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
    1.28  
    1.29  
    1.30  local
    1.31 @@ -1514,7 +1514,7 @@
    1.32        |> put_facts loc args'
    1.33        |> note_thmss_registrations kind loc args'
    1.34        |> note_thmss_qualified kind loc facts';
    1.35 -  in ((thy', ctxt'), result) end;
    1.36 +  in (result, (thy', ctxt')) end;
    1.37  
    1.38  in
    1.39