src/Pure/consts.ML

--- a/src/Pure/consts.ML	Sun Nov 11 19:41:26 2007 +0100
+++ b/src/Pure/consts.ML	Sun Nov 11 20:29:04 2007 +0100
@@ -12,7 +12,7 @@
   val eq_consts: T * T -> bool
   val abbrevs_of: T -> string list -> (term * term) list
   val dest: T ->
-   {constants: (typ * (term * term) option) NameSpace.table,
+   {constants: (typ * term option) NameSpace.table,
     constraints: typ NameSpace.table}
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
@@ -48,9 +48,7 @@
 (* datatype T *)
 
 type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool};
-
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
-fun dest_abbrev ({rhs, normal_rhs, ...}: abbrev) = (rhs, normal_rhs);
 
 datatype T = Consts of
  {decls: ((decl * abbrev option) * serial) NameSpace.table,
@@ -74,7 +72,7 @@
 fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
  {constants = (space,
     Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
-      Symtab.update (c, (T, Option.map dest_abbrev abbr))) decls Symtab.empty),
+      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
   constraints = (space, constraints)};
 
 
@@ -272,9 +270,9 @@
     val rhs = raw_rhs
       |> Term.map_types (Type.cert_typ tsig)
       |> cert_term;
+    val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
     val lhs = Const (NameSpace.full naming c, T);
-    val rhs' = expand_term rhs;
 
     fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
       Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
@@ -284,7 +282,7 @@
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
         val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
-        val abbr = {rhs = rhs, normal_rhs = rhs', force_expand = force_expand};
+        val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val decls' = decls
           |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
         val rev_abbrevs' = rev_abbrevs