src/Pure/Isar/theory_target.ML
changeset 25028 e0f74efc210f
parent 25022 bb0dcb603a13
child 25040 4e54c5ae6852
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sun Oct 14 00:18:09 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Oct 14 00:18:11 2007 +0200
     1.3 @@ -16,9 +16,6 @@
     1.4  structure TheoryTarget: THEORY_TARGET =
     1.5  struct
     1.6  
     1.7 -
     1.8 -(** locale targets **)
     1.9 -
    1.10  (* context data *)
    1.11  
    1.12  datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    1.13 @@ -203,7 +200,7 @@
    1.14          val t = Term.list_comb (const, map Free xs);
    1.15        in (((c, mx2), t), thy') end;
    1.16      fun const_class ((c, _), mx) (_, t) =
    1.17 -      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, t), mx))
    1.18 +      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), t))
    1.19        #-> Class.remove_constraint target;
    1.20  
    1.21      val (abbrs, lthy') = lthy
    1.22 @@ -212,7 +209,7 @@
    1.23      lthy'
    1.24      |> is_class ? fold2 const_class decls abbrs
    1.25      |> is_locale ? fold (internal_abbrev ta Syntax.mode_default) abbrs
    1.26 -    |> LocalDefs.add_defs (map (apsnd (pair ("", []))) abbrs) |>> map (apsnd snd)
    1.27 +    |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
    1.28    end;
    1.29  
    1.30  
    1.31 @@ -244,8 +241,8 @@
    1.32      |-> (fn (lhs, rhs) =>
    1.33            LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
    1.34            #> is_locale ? internal_abbrev ta prmode ((c, mx2), Term.list_comb (lhs, xs))
    1.35 -          #> is_class ? add_abbrev_in_class ((c, Term.list_comb (lhs, xs)), mx1))
    1.36 -    |> LocalDefs.add_defs [((c, NoSyn), (("", []), raw_t))] |>> the_single
    1.37 +          #> is_class ? add_abbrev_in_class ((c, mx1), Term.list_comb (lhs, xs)))
    1.38 +    |> LocalDefs.add_def ((c, NoSyn), raw_t)
    1.39    end;
    1.40  
    1.41  
    1.42 @@ -315,7 +312,7 @@
    1.43    let
    1.44      val thy = ProofContext.theory_of ctxt;
    1.45      val is_locale = target <> "";
    1.46 -    val is_class = is_some (Class.class_of_locale thy target);
    1.47 +    val is_class = Class.is_class thy target;
    1.48      val ta = Target {target = target, is_locale = is_locale, is_class = is_class};
    1.49    in
    1.50      ctxt
    1.51 @@ -332,8 +329,7 @@
    1.52        declaration = declaration ta,
    1.53        target_naming = target_naming ta,
    1.54        reinit = fn _ =>
    1.55 -        (if is_locale then Locale.init target else ProofContext.init)
    1.56 -        #> begin target,
    1.57 +        begin target o (if is_locale then Locale.init target else ProofContext.init),
    1.58        exit = LocalTheory.target_of}
    1.59    end;
    1.60