tuned Consts signature;
authorwenzelm
Sat Dec 09 18:05:41 2006 +0100 (2006-12-09)
changeset 2172225239591e732
parent 21721 908a93216f00
child 21723 88661e47147d
tuned Consts signature;
src/Pure/Tools/codegen_package.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Sat Dec 09 18:05:40 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Sat Dec 09 18:05:41 2006 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4    let
     1.5      val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
     1.6      val idf = CodegenNames.const thy c';
     1.7 -    val ty_decl = Consts.declaration consts idf;
     1.8 +    val ty_decl = Consts.the_declaration consts idf;
     1.9      val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
    1.10        (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
    1.11      val _ = if exists not (map (Sign.of_sort thy) insts)
     2.1 --- a/src/Pure/sign.ML	Sat Dec 09 18:05:40 2006 +0100
     2.2 +++ b/src/Pure/sign.ML	Sat Dec 09 18:05:41 2006 +0100
     2.3 @@ -285,11 +285,11 @@
     2.4  (* polymorphic constants *)
     2.5  
     2.6  val consts_of = #consts o rep_sg;
     2.7 -val the_const_constraint = Consts.constraint o consts_of;
     2.8 +val the_const_constraint = Consts.the_constraint o consts_of;
     2.9  val const_constraint = try o the_const_constraint;
    2.10 -val the_const_type = Consts.declaration o consts_of;
    2.11 +val the_const_type = Consts.the_declaration o consts_of;
    2.12  val const_type = try o the_const_type;
    2.13 -val const_monomorphic = Consts.monomorphic o consts_of;
    2.14 +val const_monomorphic = Consts.is_monomorphic o consts_of;
    2.15  val const_syntax_name = Consts.syntax_name o consts_of;
    2.16  val const_typargs = Consts.typargs o consts_of;
    2.17  val const_instance = Consts.instance o consts_of;
    2.18 @@ -585,7 +585,7 @@
    2.19        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
    2.20  
    2.21      fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
    2.22 -        (try (Consts.constraint consts)) def_type def_sort (Consts.intern consts)
    2.23 +        (try (Consts.the_constraint consts)) def_type def_sort (Consts.intern consts)
    2.24          (intern_tycons thy) (intern_sort thy) used freeze typs ts)
    2.25        handle TYPE (msg, _, _) => Exn (ERROR msg);
    2.26  
    2.27 @@ -758,7 +758,7 @@
    2.28      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    2.29        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    2.30      val (res, consts') = consts_of thy
    2.31 -      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true);
    2.32 +      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode (c, t);
    2.33    in (res, thy |> map_consts (K consts')) end;
    2.34  
    2.35