# HG changeset patch
# User wenzelm
# Date 1165952961 -3600
# Node ID 1a9f57f1bc3ada39ec3b006aa7ee6f089779c580
# Parent  74409847e349b065ab07a83e67e41afeeb4cf1fb
abbreviate: tuned signature;

diff -r 74409847e349 -r 1a9f57f1bc3a src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Dec 12 20:49:19 2006 +0100
+++ b/src/Pure/consts.ML	Tue Dec 12 20:49:21 2006 +0100
@@ -32,7 +32,7 @@
   val constrain: string * typ option -> T -> T
   val set_expand: bool -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
-    bstring * term -> T -> ((string * typ) * term) * T
+    bstring * term -> T -> (term * term) * T
   val hide: bool -> string -> T -> T
   val empty: T
   val merge: T * T -> T
@@ -269,11 +269,9 @@
     val rhs = raw_rhs
       |> Term.map_types (Type.cert_typ tsig)
       |> cert_term;
+    val T = Term.fastype_of rhs;
+    val lhs = Const (NameSpace.full naming c, T);
     val rhs' = expand_term rhs;
-    val T = Term.fastype_of rhs;
-
-    val const = (NameSpace.full naming c, T);
-    val lhs = Const const;
 
     fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
       Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
@@ -287,7 +285,7 @@
         val rev_abbrevs' = rev_abbrevs
           |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs', do_expand) end)
-    |> pair (const, rhs)
+    |> pair (lhs, rhs)
   end;
 
 end;