src/Pure/Isar/proof.ML
changeset 13335 7995b3f4ca5e
parent 13297 e4ae0732e2be
child 13377 cc8245843abc
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jul 10 14:49:06 2002 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jul 10 14:50:08 2002 +0200
     1.3 @@ -818,12 +818,12 @@
     1.4        |> (case locale_spec of None => I | Some (loc, (loc_atts, loc_attss)) => fn thy =>
     1.5          if length names <> length loc_attss then
     1.6            raise THEORY ("Bad number of locale attributes", [thy])
     1.7 -        else (locale_ctxt, thy)
     1.8 +        else (thy, locale_ctxt)
     1.9            |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
    1.10 -          |> (fn ((ctxt', thy'), res) =>
    1.11 +          |> (fn ((thy', ctxt'), res) =>
    1.12              if name = "" andalso null loc_atts then thy'
    1.13 -            else (ctxt', thy')
    1.14 -              |> (#2 o #1 o Locale.add_thmss loc [((name, flat res), loc_atts)])))
    1.15 +            else (thy', ctxt')
    1.16 +              |> (#1 o #1 o Locale.add_thmss loc [((name, flat res), loc_atts)])))
    1.17        |> Locale.smart_have_thmss k locale_spec
    1.18          ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
    1.19        |> (fn (thy, res) => (thy, res)