src/Pure/consts.ML
changeset 21794 1a9f57f1bc3a
parent 21720 059e6b8cee8e
child 21822 5a279c9138b6
     1.1 --- a/src/Pure/consts.ML	Tue Dec 12 20:49:19 2006 +0100
     1.2 +++ b/src/Pure/consts.ML	Tue Dec 12 20:49:21 2006 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    val constrain: string * typ option -> T -> T
     1.5    val set_expand: bool -> T -> T
     1.6    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
     1.7 -    bstring * term -> T -> ((string * typ) * term) * T
     1.8 +    bstring * term -> T -> (term * term) * T
     1.9    val hide: bool -> string -> T -> T
    1.10    val empty: T
    1.11    val merge: T * T -> T
    1.12 @@ -269,11 +269,9 @@
    1.13      val rhs = raw_rhs
    1.14        |> Term.map_types (Type.cert_typ tsig)
    1.15        |> cert_term;
    1.16 +    val T = Term.fastype_of rhs;
    1.17 +    val lhs = Const (NameSpace.full naming c, T);
    1.18      val rhs' = expand_term rhs;
    1.19 -    val T = Term.fastype_of rhs;
    1.20 -
    1.21 -    val const = (NameSpace.full naming c, T);
    1.22 -    val lhs = Const const;
    1.23  
    1.24      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.25        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    1.26 @@ -287,7 +285,7 @@
    1.27          val rev_abbrevs' = rev_abbrevs
    1.28            |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
    1.29        in (decls', constraints, rev_abbrevs', do_expand) end)
    1.30 -    |> pair (const, rhs)
    1.31 +    |> pair (lhs, rhs)
    1.32    end;
    1.33  
    1.34  end;