# HG changeset patch
# User wenzelm
# Date 1272444694 -7200
# Node ID edb757388592a3910464ee1ed6fcc3de27e01d9f
# Parent  c311bd68f9190045b5f18f2c44cab5ad0f9048d5
get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
tuned;

diff -r c311bd68f919 -r edb757388592 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 10:43:08 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 10:51:34 2010 +0200
@@ -608,22 +608,19 @@
 
 (* types *)
 
-fun get_sort ctxt raw_env =
+fun get_sort ctxt raw_text =
   let
-    val thy = theory_of ctxt;
     val tsig = tsig_of ctxt;
 
-    fun eq ((xi, S), (xi', S')) =
-      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
-    val env = distinct eq raw_env;
+    val text = distinct (op =) (map (apsnd (Type.minimize_sort tsig)) raw_text);
     val _ =
-      (case duplicates (eq_fst (op =)) env of
+      (case duplicates (eq_fst (op =)) text of
         [] => ()
       | dups => error ("Inconsistent sort constraints for type variable(s) "
           ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
 
     fun lookup xi =
-      (case AList.lookup (op =) env xi of
+      (case AList.lookup (op =) text xi of
         NONE => NONE
       | SOME S => if S = dummyS then NONE else SOME S);
 
@@ -637,7 +634,7 @@
           else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
             " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
             " for type variable " ^ quote (Term.string_of_vname' xi)));
-  in Sign.minimize_sort thy o get end;
+  in get end;
 
 fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
 fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
@@ -737,11 +734,10 @@
 
 fun parse_sort ctxt text =
   let
-    val thy = theory_of ctxt;
     val (syms, pos) = Syntax.parse_token Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
       handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
-  in Sign.minimize_sort thy S end;
+  in Type.minimize_sort (tsig_of ctxt) S end;
 
 fun parse_typ ctxt text =
   let
diff -r c311bd68f919 -r edb757388592 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Apr 28 10:43:08 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Apr 28 10:51:34 2010 +0200
@@ -110,8 +110,7 @@
 
 fun decode_term get_sort map_const map_free tm =
   let
-    val sort_env = term_sorts tm;
-    val decodeT = typ_of_term (get_sort sort_env);
+    val decodeT = typ_of_term (get_sort (term_sorts tm));
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
           type_constraint (decodeT typ) (decode t)