src/Pure/Isar/proof_context.ML
changeset 25052 a014d544f54d
parent 25039 06ed511837d5
child 25060 17c313217998
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 17:06:15 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 17:06:18 2007 +0200
     1.3 @@ -144,6 +144,7 @@
     1.4    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
     1.5    val add_abbrev: string -> Markup.property list ->
     1.6      bstring * term -> Proof.context -> (term * term) * Proof.context
     1.7 +  val revert_abbrev: string -> string -> Proof.context -> Proof.context
     1.8    val verbose: bool ref
     1.9    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.10    val print_syntax: Proof.context -> unit
    1.11 @@ -259,7 +260,7 @@
    1.12  val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
    1.13  val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
    1.14  
    1.15 -val consts_of = fst o #consts o rep_context;
    1.16 +val consts_of = #1 o #consts o rep_context;
    1.17  val const_syntax_name = Consts.syntax_name o consts_of;
    1.18  val the_const_constraint = Consts.the_constraint o consts_of;
    1.19  
    1.20 @@ -429,12 +430,8 @@
    1.21      val consts = consts_of ctxt;
    1.22      val Mode {abbrev, ...} = get_mode ctxt;
    1.23    in
    1.24 -    if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t)
    1.25 -    then t
    1.26 -    else
    1.27 -      t
    1.28 -      |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) []
    1.29 -      |> Pattern.rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM]) []
    1.30 +    if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
    1.31 +    else t |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) []
    1.32    end;
    1.33  
    1.34  
    1.35 @@ -1042,6 +1039,8 @@
    1.36      |> pair (lhs, rhs)
    1.37    end;
    1.38  
    1.39 +fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
    1.40 +
    1.41  
    1.42  (* fixes *)
    1.43  
    1.44 @@ -1195,7 +1194,7 @@
    1.45  
    1.46  fun pretty_abbrevs show_globals ctxt =
    1.47    let
    1.48 -    val ((_, globals), (space, consts)) =
    1.49 +    val ((space, consts), (_, globals)) =
    1.50        pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
    1.51      fun add_abbr (_, (_, NONE)) = I
    1.52        | add_abbr (c, (T, SOME (t, _))) =