src/Pure/Isar/theory_target.ML
changeset 24914 95cda5dd58d5
parent 24911 4efb68e5576d
child 24935 a033971c63a0
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 08 20:20:13 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 08 22:03:21 2007 +0200
     1.3 @@ -118,9 +118,10 @@
     1.4          val mx3 = if is_loc then NoSyn else mx1;
     1.5          val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
     1.6        in (((c, mx2), t), thy') end;
     1.7 -
     1.8      fun const_class (SOME class) ((c, _), mx) (_, t) =
     1.9 -          Class.add_const_in_class class ((c, t), mx)
    1.10 +          LocalTheory.raw_theory_result
    1.11 +            (Class.add_const_in_class class ((c, t), mx))
    1.12 +          #-> (fn c => Class.remove_constraint [class] c)
    1.13        | const_class NONE _ _ = I;
    1.14      fun hide_abbrev (SOME class) abbrs thy =
    1.15            let
    1.16 @@ -137,13 +138,14 @@
    1.17              Sign.hide_consts_i true cs thy
    1.18            end
    1.19        | hide_abbrev NONE _ thy = thy;
    1.20 +
    1.21      val (abbrs, lthy') = lthy
    1.22        |> LocalTheory.theory_result (fold_map const decls)
    1.23      val defs = map (apsnd (pair ("", []))) abbrs;
    1.24  
    1.25    in
    1.26      lthy'
    1.27 -    |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
    1.28 +    |> fold2 (const_class some_class) decls abbrs
    1.29      |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
    1.30      |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
    1.31          (*FIXME abbreviations should never occur*)
    1.32 @@ -184,17 +186,17 @@
    1.33      val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
    1.34      val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
    1.35      val mx3 = if is_loc then NoSyn else mx1;
    1.36 -    fun add_abbrev_in_class NONE = K I
    1.37 -      | add_abbrev_in_class (SOME class) =
    1.38 -          Class.add_abbrev_in_class class prmode;
    1.39 +    fun add_abbrev_in_class (SOME class) abbr =
    1.40 +          LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr)
    1.41 +          #-> (fn c => Class.remove_constraint [class] c)
    1.42 +      | add_abbrev_in_class NONE _ = I;
    1.43    in
    1.44      lthy
    1.45      |> LocalTheory.theory_result
    1.46          (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
    1.47      |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
    1.48      #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    1.49 -    #> LocalTheory.raw_theory
    1.50 -         (add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1))
    1.51 +    #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    1.52      #> local_abbrev (c, rhs))
    1.53    end;
    1.54