# HG changeset patch
# User haftmann
# Date 1385624114 -3600
# Node ID 1512fa5fe531f05fb1389ec864c9d7cbf0fe26f0
# Parent  89d5b69e5a081ab9c79a29ffb82faaa19a6f524e
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate

diff -r 89d5b69e5a08 -r 1512fa5fe531 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Nov 28 08:34:52 2013 +0100
+++ b/src/Pure/Isar/code.ML	Thu Nov 28 08:35:14 2013 +0100
@@ -140,7 +140,7 @@
 fun check_unoverload thy (c, ty) =
   let
     val c' = Axclass.unoverload_const thy (c, ty);
-    val ty_decl = Sign.the_const_type thy c';
+    val ty_decl = const_typ thy c';
   in
     if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
     then c'
@@ -450,7 +450,7 @@
 
 fun check_decl_ty thy (c, ty) =
   let
-    val ty_decl = Sign.the_const_type thy c;
+    val ty_decl = const_typ thy c;
   in if typscheme_equiv (ty_decl, ty) then ()
     else bad_thm ("Type\n" ^ string_of_typ thy ty
       ^ "\nof constant " ^ quote c
@@ -1124,7 +1124,7 @@
     val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
     val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
     val (ws, vs) = chop pos zs;
-    val T = devarify (Sign.the_const_type thy case_const);
+    val T = devarify (const_typ thy case_const);
     val Ts = binder_types T;
     val T_cong = nth Ts pos;
     fun mk_prem z = Free (z, T_cong);