# HG changeset patch
# User wenzelm
# Date 1147102808 -7200
# Node ID 856cd74601685bc33aefe805169a797629ff4279
# Parent  e7036e812702e596f1c5959e41a704277ec3aee8
Defs.define: const_typargs;

diff -r e7036e812702 -r 856cd7460168 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon May 08 17:40:07 2006 +0200
+++ b/src/Pure/theory.ML	Mon May 08 17:40:08 2006 +0200
@@ -266,7 +266,7 @@
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in
-    defs |> Defs.define (Sign.the_const_type thy) true (Context.theory_name thy)
+    defs |> Defs.define (Sign.const_typargs thy) true (Context.theory_name thy)
       name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
@@ -302,7 +302,7 @@
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) = Defs.define (Sign.the_const_type thy) false (Context.theory_name thy)
+    fun specify (c, T) = Defs.define (Sign.const_typargs thy) false (Context.theory_name thy)
       (c ^ " axiom") (prep_const thy (c, T)) [];
     val finalize = specify o check_overloading thy overloaded o
       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;