add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
authorwenzelm
Tue Oct 16 17:06:11 2007 +0200 (2007-10-16)
changeset 25049ec0547a4fcf0
parent 25048 5a94a87af697
child 25050 0dc445970b4b
add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
added revert_abbrev;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Oct 16 17:06:09 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 16 17:06:11 2007 +0200
     1.3 @@ -160,6 +160,7 @@
     1.4    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.5    val add_abbrev: string -> Markup.property list ->
     1.6      bstring * term -> theory -> (term * term) * theory
     1.7 +  val revert_abbrev: string -> string -> theory -> theory
     1.8    include SIGN_THEORY
     1.9    val add_const_constraint: string * typ option -> theory -> theory
    1.10    val primitive_class: string * class list -> theory -> theory
    1.11 @@ -702,19 +703,19 @@
    1.12  end;
    1.13  
    1.14  
    1.15 -(* add abbreviations *)
    1.16 +(* abbreviations *)
    1.17  
    1.18  fun add_abbrev mode tags (c, raw_t) thy =
    1.19    let
    1.20      val pp = pp thy;
    1.21 -    val prep_tm = Compress.term thy o no_frees pp o
    1.22 -      map_types Logic.legacy_varifyT (* FIXME tmp *) o
    1.23 -      Term.no_dummy_patterns o cert_term_abbrev thy;
    1.24 +    val prep_tm = Compress.term thy o no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.25      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.26        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.27      val (res, consts') = consts_of thy
    1.28        |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
    1.29 -  in (pairself Logic.unvarify res, thy |> map_consts (K consts')) end;
    1.30 +  in (res, thy |> map_consts (K consts')) end;
    1.31 +
    1.32 +fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
    1.33  
    1.34  
    1.35  (* add constraints *)