# HG changeset patch
# User wenzelm
# Date 1165683941 -3600
# Node ID 25239591e732212093e9f6e1705f6261eb8ab519
# Parent  908a93216f00b37f461108cf7148d19d7d8971cf
tuned Consts signature;

diff -r 908a93216f00 -r 25239591e732 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Sat Dec 09 18:05:40 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Sat Dec 09 18:05:41 2006 +0100
@@ -211,7 +211,7 @@
   let
     val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
     val idf = CodegenNames.const thy c';
-    val ty_decl = Consts.declaration consts idf;
+    val ty_decl = Consts.the_declaration consts idf;
     val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
       (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
     val _ = if exists not (map (Sign.of_sort thy) insts)
diff -r 908a93216f00 -r 25239591e732 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Dec 09 18:05:40 2006 +0100
+++ b/src/Pure/sign.ML	Sat Dec 09 18:05:41 2006 +0100
@@ -285,11 +285,11 @@
 (* polymorphic constants *)
 
 val consts_of = #consts o rep_sg;
-val the_const_constraint = Consts.constraint o consts_of;
+val the_const_constraint = Consts.the_constraint o consts_of;
 val const_constraint = try o the_const_constraint;
-val the_const_type = Consts.declaration o consts_of;
+val the_const_type = Consts.the_declaration o consts_of;
 val const_type = try o the_const_type;
-val const_monomorphic = Consts.monomorphic o consts_of;
+val const_monomorphic = Consts.is_monomorphic o consts_of;
 val const_syntax_name = Consts.syntax_name o consts_of;
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;
@@ -585,7 +585,7 @@
       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
 
     fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
-        (try (Consts.constraint consts)) def_type def_sort (Consts.intern consts)
+        (try (Consts.the_constraint consts)) def_type def_sort (Consts.intern consts)
         (intern_tycons thy) (intern_sort thy) used freeze typs ts)
       handle TYPE (msg, _, _) => Exn (ERROR msg);
 
@@ -758,7 +758,7 @@
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true);
+      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode (c, t);
   in (res, thy |> map_consts (K consts')) end;