1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 10:43:08 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 10:51:34 2010 +0200
     1.3 @@ -608,22 +608,19 @@
     1.4  
     1.5  (* types *)
     1.6  
     1.7 -fun get_sort ctxt raw_env =
     1.8 +fun get_sort ctxt raw_text =
     1.9    let
    1.10 -    val thy = theory_of ctxt;
    1.11      val tsig = tsig_of ctxt;
    1.12  
    1.13 -    fun eq ((xi, S), (xi', S')) =
    1.14 -      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
    1.15 -    val env = distinct eq raw_env;
    1.16 +    val text = distinct (op =) (map (apsnd (Type.minimize_sort tsig)) raw_text);
    1.17      val _ =
    1.18 -      (case duplicates (eq_fst (op =)) env of
    1.19 +      (case duplicates (eq_fst (op =)) text of
    1.20          [] => ()
    1.21        | dups => error ("Inconsistent sort constraints for type variable(s) "
    1.22            ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
    1.23  
    1.24      fun lookup xi =
    1.25 -      (case AList.lookup (op =) env xi of
    1.26 +      (case AList.lookup (op =) text xi of
    1.27          NONE => NONE
    1.28        | SOME S => if S = dummyS then NONE else SOME S);
    1.29  
    1.30 @@ -637,7 +634,7 @@
    1.31            else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
    1.32              " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
    1.33              " for type variable " ^ quote (Term.string_of_vname' xi)));
    1.34 -  in Sign.minimize_sort thy o get end;
    1.35 +  in get end;
    1.36  
    1.37  fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
    1.38  fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
    1.39 @@ -737,11 +734,10 @@
    1.40  
    1.41  fun parse_sort ctxt text =
    1.42    let
    1.43 -    val thy = theory_of ctxt;
    1.44      val (syms, pos) = Syntax.parse_token Markup.sort text;
    1.45      val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
    1.46        handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    1.47 -  in Sign.minimize_sort thy S end;
    1.48 +  in Type.minimize_sort (tsig_of ctxt) S end;
    1.49  
    1.50  fun parse_typ ctxt text =
    1.51    let

     2.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Apr 28 10:43:08 2010 +0200
     2.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Apr 28 10:51:34 2010 +0200
     2.3 @@ -110,8 +110,7 @@
     2.4  
     2.5  fun decode_term get_sort map_const map_free tm =
     2.6    let
     2.7 -    val sort_env = term_sorts tm;
     2.8 -    val decodeT = typ_of_term (get_sort sort_env);
     2.9 +    val decodeT = typ_of_term (get_sort (term_sorts tm));
    2.10  
    2.11      fun decode (Const ("_constrain", _) $ t $ typ) =
    2.12            type_constraint (decodeT typ) (decode t)