src/Pure/sign.ML

--- a/src/Pure/sign.ML	Thu Dec 07 17:58:45 2006 +0100
+++ b/src/Pure/sign.ML	Thu Dec 07 17:58:46 2006 +0100
@@ -192,8 +192,8 @@
   val read_prop: theory -> string -> term
   val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
   val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory ->
-    (term * term) list * theory
+  val add_abbrevs: string -> (bstring * term) list -> theory ->
+    ((string * typ) * term) list * theory
   include SIGN_THEORY
 end
 
@@ -751,22 +751,16 @@
 end;
 
 
-(* add abbreviations -- cf. ProofContext.add_abbrevs *)
+(* add abbreviations *)
 
-fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
+fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn thy =>
   let
-    val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
     val prep_tm = Compress.term thy 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 (((full_c, T), rhs), consts') = consts_of thy
-      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true);
-  in
-    thy
-    |> map_consts (K consts')
-    |> add_modesyntax_i prmode [(Syntax.constN ^ full_c, T, mx)]
-    |> pair (Const (full_c, T), rhs)
-  end);
+    val (res, consts') = consts_of thy
+      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true);
+  in (res, thy |> map_consts (K consts')) end);
 
 
 (* add constraints *)