src/Pure/consts.ML
changeset 21680 5d2230ad1261
parent 21205 dfe338ec9f9c
child 21694 9f65fecb6e10
     1.1 --- a/src/Pure/consts.ML	Wed Dec 06 21:18:56 2006 +0100
     1.2 +++ b/src/Pure/consts.ML	Wed Dec 06 21:18:57 2006 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    val constrain: string * typ option -> T -> T
     1.5    val expand_abbrevs: bool -> T -> T
     1.6    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
     1.7 -    (bstring * term) * bool -> T -> T
     1.8 +    (bstring * term) * bool -> T -> ((string * typ) * term) * T
     1.9    val hide: bool -> string -> T -> T
    1.10    val empty: T
    1.11    val merge: T * T -> T
    1.12 @@ -253,20 +253,27 @@
    1.13  
    1.14  fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
    1.15    let
    1.16 +    val full_c = NameSpace.full naming c;
    1.17      val rhs = raw_rhs
    1.18        |> Term.map_types (Type.cert_typ tsig)
    1.19        |> certify pp tsig (consts |> expand_abbrevs false);
    1.20      val rhs' = rhs
    1.21        |> certify pp tsig (consts |> expand_abbrevs true);
    1.22      val T = Term.fastype_of rhs;
    1.23 +
    1.24 +    fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.25 +      Pretty.string_of_term pp (Logic.mk_equals (Const (full_c, T), rhs)));
    1.26 +    val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"
    1.27 +    val _ = null (Term.hidden_polymorphism rhs T) orelse err "Extra type variables";
    1.28    in
    1.29      consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
    1.30        let
    1.31          val decls' = decls
    1.32            |> extend_decls naming (c, (((T, Abbreviation rhs'), authentic), serial ()));
    1.33          val rev_abbrevs' = rev_abbrevs
    1.34 -          |> fold (curry Symtab.update_list mode) (rev_abbrev (NameSpace.full naming c, T) rhs);
    1.35 +          |> fold (curry Symtab.update_list mode) (rev_abbrev (full_c, T) rhs);
    1.36        in (decls', constraints, rev_abbrevs', expand_abbrevs) end)
    1.37 +    |> pair ((full_c, T), rhs)
    1.38    end;
    1.39  
    1.40  end;