# HG changeset patch
# User wenzelm
# Date 1192547171 -7200
# Node ID ec0547a4fcf039ffb47bdb3ca8b1a4a912dca851
# Parent  5a94a87af69759f2fc3357dedb5694dbec24ad5b
add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
added revert_abbrev;

diff -r 5a94a87af697 -r ec0547a4fcf0 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Oct 16 17:06:09 2007 +0200
+++ b/src/Pure/sign.ML	Tue Oct 16 17:06:11 2007 +0200
@@ -160,6 +160,7 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> Markup.property list ->
     bstring * term -> theory -> (term * term) * theory
+  val revert_abbrev: string -> string -> theory -> theory
   include SIGN_THEORY
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: string * class list -> theory -> theory
@@ -702,19 +703,19 @@
 end;
 
 
-(* add abbreviations *)
+(* abbreviations *)
 
 fun add_abbrev mode tags (c, raw_t) thy =
   let
     val pp = pp thy;
-    val prep_tm = Compress.term thy o no_frees pp o
-      map_types Logic.legacy_varifyT (* FIXME tmp *) o
-      Term.no_dummy_patterns o cert_term_abbrev thy;
+    val prep_tm = Compress.term thy o no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val (res, consts') = consts_of thy
       |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
-  in (pairself Logic.unvarify res, thy |> map_consts (K consts')) end;
+  in (res, thy |> map_consts (K consts')) end;
+
+fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
 
 
 (* add constraints *)