simplified Consts.dest;
authorwenzelm
Sun Nov 11 20:29:04 2007 +0100 (2007-11-11 ago)
changeset 254041a58d1c9fe88
parent 25403 359b179fc963
child 25405 7ac8c93be624
simplified Consts.dest;
dest;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Sun Nov 11 19:41:26 2007 +0100
     1.2 +++ b/src/Pure/consts.ML	Sun Nov 11 20:29:04 2007 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val eq_consts: T * T -> bool
     1.5    val abbrevs_of: T -> string list -> (term * term) list
     1.6    val dest: T ->
     1.7 -   {constants: (typ * (term * term) option) NameSpace.table,
     1.8 +   {constants: (typ * term option) NameSpace.table,
     1.9      constraints: typ NameSpace.table}
    1.10    val the_type: T -> string -> typ                             (*exception TYPE*)
    1.11    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
    1.12 @@ -48,9 +48,7 @@
    1.13  (* datatype T *)
    1.14  
    1.15  type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool};
    1.16 -
    1.17  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
    1.18 -fun dest_abbrev ({rhs, normal_rhs, ...}: abbrev) = (rhs, normal_rhs);
    1.19  
    1.20  datatype T = Consts of
    1.21   {decls: ((decl * abbrev option) * serial) NameSpace.table,
    1.22 @@ -74,7 +72,7 @@
    1.23  fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
    1.24   {constants = (space,
    1.25      Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
    1.26 -      Symtab.update (c, (T, Option.map dest_abbrev abbr))) decls Symtab.empty),
    1.27 +      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
    1.28    constraints = (space, constraints)};
    1.29  
    1.30  
    1.31 @@ -272,9 +270,9 @@
    1.32      val rhs = raw_rhs
    1.33        |> Term.map_types (Type.cert_typ tsig)
    1.34        |> cert_term;
    1.35 +    val normal_rhs = expand_term rhs;
    1.36      val T = Term.fastype_of rhs;
    1.37      val lhs = Const (NameSpace.full naming c, T);
    1.38 -    val rhs' = expand_term rhs;
    1.39  
    1.40      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.41        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    1.42 @@ -284,7 +282,7 @@
    1.43      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.44        let
    1.45          val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
    1.46 -        val abbr = {rhs = rhs, normal_rhs = rhs', force_expand = force_expand};
    1.47 +        val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    1.48          val decls' = decls
    1.49            |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
    1.50          val rev_abbrevs' = rev_abbrevs