1.1 --- a/src/Pure/Isar/code.ML	Thu Nov 28 08:34:52 2013 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Nov 28 08:35:14 2013 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  fun check_unoverload thy (c, ty) =
     1.5    let
     1.6      val c' = Axclass.unoverload_const thy (c, ty);
     1.7 -    val ty_decl = Sign.the_const_type thy c';
     1.8 +    val ty_decl = const_typ thy c';
     1.9    in
    1.10      if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
    1.11      then c'
    1.12 @@ -450,7 +450,7 @@
    1.13  
    1.14  fun check_decl_ty thy (c, ty) =
    1.15    let
    1.16 -    val ty_decl = Sign.the_const_type thy c;
    1.17 +    val ty_decl = const_typ thy c;
    1.18    in if typscheme_equiv (ty_decl, ty) then ()
    1.19      else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.20        ^ "\nof constant " ^ quote c
    1.21 @@ -1124,7 +1124,7 @@
    1.22      val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
    1.23      val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
    1.24      val (ws, vs) = chop pos zs;
    1.25 -    val T = devarify (Sign.the_const_type thy case_const);
    1.26 +    val T = devarify (const_typ thy case_const);
    1.27      val Ts = binder_types T;
    1.28      val T_cong = nth Ts pos;
    1.29      fun mk_prem z = Free (z, T_cong);