1.1 --- a/src/Pure/sign.ML	Mon Oct 15 21:08:35 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 15 21:08:36 2007 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  
     1.5  val consts_of = #consts o rep_sg;
     1.6  val the_const_constraint = Consts.the_constraint o consts_of;
     1.7 -val the_const_type = Consts.the_declaration o consts_of;
     1.8 +val the_const_type = Consts.the_type o consts_of;
     1.9  val const_type = try o the_const_type;
    1.10  val const_monomorphic = Consts.is_monomorphic o consts_of;
    1.11  val const_syntax_name = Consts.syntax_name o consts_of;

     2.1 --- a/src/Tools/code/code_thingol.ML	Mon Oct 15 21:08:35 2007 +0200
     2.2 +++ b/src/Tools/code/code_thingol.ML	Mon Oct 15 21:08:36 2007 +0200
     2.3 @@ -427,7 +427,7 @@
     2.4    end
     2.5  and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
     2.6    let
     2.7 -    val ty_decl = Consts.the_declaration consts c;
     2.8 +    val ty_decl = Consts.the_type consts c;
     2.9      val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
    2.10      val sorts = map (snd o dest_TVar) tys_decl;
    2.11    in