Defs.define: const_typargs;
authorwenzelm
Mon May 08 17:40:08 2006 +0200 (2006-05-08)
changeset 19592856cd7460168
parent 19591 e7036e812702
child 19593 c52a4360a41d
Defs.define: const_typargs;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Mon May 08 17:40:07 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon May 08 17:40:08 2006 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     1.5      val _ = check_overloading thy overloaded lhs_const;
     1.6    in
     1.7 -    defs |> Defs.define (Sign.the_const_type thy) true (Context.theory_name thy)
     1.8 +    defs |> Defs.define (Sign.const_typargs thy) true (Context.theory_name thy)
     1.9        name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
    1.10    end
    1.11    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.12 @@ -302,7 +302,7 @@
    1.13      fun const_of (Const const) = const
    1.14        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.15        | const_of _ = error "Attempt to finalize non-constant term";
    1.16 -    fun specify (c, T) = Defs.define (Sign.the_const_type thy) false (Context.theory_name thy)
    1.17 +    fun specify (c, T) = Defs.define (Sign.const_typargs thy) false (Context.theory_name thy)
    1.18        (c ^ " axiom") (prep_const thy (c, T)) [];
    1.19      val finalize = specify o check_overloading thy overloaded o
    1.20        const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;