src/Pure/Isar/isar_thy.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18421 464c93701351
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -11,14 +11,14 @@
     1.4    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
     1.5    val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
     1.6    val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
     1.7 -  val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
     1.8 -  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
     1.9 +  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    1.10 +  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
    1.11    val theorems: string ->
    1.12      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.13 -    -> theory -> theory * (string * thm list) list
    1.14 +    -> theory -> (string * thm list) list * theory 
    1.15    val theorems_i: string ->
    1.16      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
    1.17 -    -> theory -> theory * (string * thm list) list
    1.18 +    -> theory -> (string * thm list) list * theory
    1.19    val smart_theorems: string -> xstring option ->
    1.20      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    1.21      theory -> theory * Proof.context
    1.22 @@ -75,21 +75,19 @@
    1.23  
    1.24  fun theorems kind args thy = thy
    1.25    |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
    1.26 -  |> tap (present_theorems kind)
    1.27 -  |> swap;
    1.28 +  |> tap (present_theorems kind);
    1.29  
    1.30  fun theorems_i kind args =
    1.31    PureThy.note_thmss_i (Drule.kind kind) args
    1.32 -  #> tap (present_theorems kind)
    1.33 -  #> swap;
    1.34 +  #> tap (present_theorems kind);
    1.35  
    1.36 -fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)];
    1.37 -fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)];
    1.38 +fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
    1.39 +fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)];
    1.40  
    1.41  fun smart_theorems kind NONE args thy = thy
    1.42        |> theorems kind args
    1.43 -      |> tap (present_theorems kind o swap)
    1.44 -      |> (fn (thy, _) => (thy, ProofContext.init thy))
    1.45 +      |> tap (present_theorems kind)
    1.46 +      |> (fn (_, thy) => (thy, ProofContext.init thy))
    1.47    | smart_theorems kind (SOME loc) args thy = thy
    1.48        |> Locale.note_thmss kind loc args
    1.49        |> tap (present_theorems kind o swap o apfst #1)