add_finals: prep_consts, i.e. varify type;
authorwenzelm
Tue Jan 24 00:43:24 2006 +0100 (2006-01-24)
changeset 18763e2b4ba340ff1
parent 18762 9098c92a945f
child 18764 3f8bcf80dc18
add_finals: prep_consts, i.e. varify type;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Jan 24 00:43:23 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Tue Jan 24 00:43:24 2006 +0100
     1.3 @@ -342,7 +342,8 @@
     1.4      fun const_of (Const const) = const
     1.5        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
     1.6        | const_of _ = error "Attempt to finalize non-constant term";
     1.7 -    fun specify (c, T) = Defs.define (Sign.the_const_type thy) (c ^ " axiom") (c, T) [];
     1.8 +    fun specify (c, T) =
     1.9 +      Defs.define (Sign.the_const_type thy) (c ^ " axiom") (prep_const thy (c, T)) [];
    1.10      val finalize = specify o check_overloading thy overloaded o
    1.11        const_of o no_vars (Sign.pp thy) o prep_term thy;
    1.12    in thy |> map_defs (fold finalize args) end;