src/Pure/Isar/isar_thy.ML
changeset 18421 464c93701351
parent 18418 bf448d999b7e
child 18562 15178f4aa203
     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)];