--- a/src/Pure/sign.ML Mon Oct 15 21:08:35 2007 +0200
+++ b/src/Pure/sign.ML Mon Oct 15 21:08:36 2007 +0200
@@ -265,7 +265,7 @@
val consts_of = #consts o rep_sg;
val the_const_constraint = Consts.the_constraint o consts_of;
-val the_const_type = Consts.the_declaration o consts_of;
+val the_const_type = Consts.the_type o consts_of;
val const_type = try o the_const_type;
val const_monomorphic = Consts.is_monomorphic o consts_of;
val const_syntax_name = Consts.syntax_name o consts_of;
--- a/src/Tools/code/code_thingol.ML Mon Oct 15 21:08:35 2007 +0200
+++ b/src/Tools/code/code_thingol.ML Mon Oct 15 21:08:36 2007 +0200
@@ -427,7 +427,7 @@
end
and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
let
- val ty_decl = Consts.the_declaration consts c;
+ val ty_decl = Consts.the_type consts c;
val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
val sorts = map (snd o dest_TVar) tys_decl;
in