sort assignment before simultaneous term_check, not isolated parse_term;
prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment;
simplified Syntax_Phases.decode_sort/decode_typ;
discontinued unused Proof_Context.check_tvar;

--- a/NEWS	Wed Nov 09 17:12:26 2011 +0100
+++ b/NEWS	Wed Nov 09 17:57:42 2011 +0100
@@ -16,6 +16,16 @@
 * Redundant attribute 'code_inline' has been discontinued. Use
 'code_unfold' instead. INCOMPATIBILITY.
 
+* Sort constraints are now propagated in simultaneous statements, just
+like type constraints.  INCOMPATIBILITY in rare situations, where
+distinct sorts used to be assigned accidentally.  For example:
+
+  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
+
+  lemma "P (x::'a)" and "Q (y::'a::bar)"
+    -- "now uniform 'a::bar instead of default sort for first occurence (!)"
+
+
 
 *** HOL ***
 

--- a/src/HOL/Tools/record.ML	Wed Nov 09 17:12:26 2011 +0100
+++ b/src/HOL/Tools/record.ML	Wed Nov 09 17:57:42 2011 +0100
@@ -652,12 +652,6 @@
 
 (** concrete syntax for records **)
 
-(* decode type *)
-
-fun decode_type ctxt t =
-  Syntax_Phases.typ_of_term (Proof_Context.get_sort ctxt (Syntax_Phases.term_sorts t)) t;
-
-
 (* parse translations *)
 
 local
@@ -694,7 +688,7 @@
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs
                       handle Fail msg => err msg;
-                    val argtypes = map (Syntax.check_typ ctxt o decode_type ctxt) args;
+                    val argtypes = map (Syntax.check_typ ctxt o Syntax_Phases.decode_typ) args;
                     val varifyT = varifyT (fold Term.maxidx_typ argtypes 0 + 1);
                     val vartypes = map varifyT types;
 
@@ -799,7 +793,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val T = decode_type ctxt t;
+    val T = Syntax_Phases.decode_typ t;
     val varifyT = varifyT (Term.maxidx_of_typ T + 1);
 
     fun strip_fields T =
@@ -844,7 +838,7 @@
   the (nested) extension types*)
 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   let
-    val T = decode_type ctxt tm;
+    val T = Syntax_Phases.decode_typ tm;
     val varifyT = varifyT (maxidx_of_typ T + 1);
 
     fun mk_type_abbr subst name args =

--- a/src/Pure/Isar/proof_context.ML	Wed Nov 09 17:12:26 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Nov 09 17:57:42 2011 +0100
@@ -72,7 +72,6 @@
   val read_const: Proof.context -> bool -> typ -> string -> term
   val allow_dummies: Proof.context -> Proof.context
   val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
-  val check_tvar: Proof.context -> indexname * sort -> indexname * sort
   val check_tfree: Proof.context -> string * sort -> string * sort
   val intern_skolem: Proof.context -> string -> string option
   val read_term_pattern: Proof.context -> string -> term
@@ -639,8 +638,7 @@
             " for type variable " ^ quote (Term.string_of_vname' xi)));
   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));
+fun check_tfree ctxt (x, S) = (x, get_sort ctxt [((x, ~1), S)] (x, ~1));
 
 
 (* certify terms *)
@@ -940,7 +938,7 @@
 
 in
 
-val read_vars = prep_vars Syntax.parse_typ false;
+val read_vars = prep_vars Syntax.read_typ false;
 val cert_vars = prep_vars (K I) true;
 
 end;

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 17:12:26 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 17:57:42 2011 +0100
@@ -7,8 +7,8 @@
 
 signature SYNTAX_PHASES =
 sig
-  val term_sorts: term -> (indexname * sort) list
-  val typ_of_term: (indexname -> sort) -> term -> typ
+  val decode_sort: term -> sort
+  val decode_typ: term -> typ
   val decode_term: Proof.context ->
     Position.report list * term Exn.result -> Position.report list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
@@ -58,11 +58,11 @@
 
 (** decode parse trees **)
 
-(* sort_of_term *)
+(* decode_sort *)
 
-fun sort_of_term tm =
+fun decode_sort tm =
   let
-    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+    fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
 
     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
 
@@ -77,52 +77,32 @@
   in sort tm end;
 
 
-(* term_sorts *)
-
-fun term_sorts tm =
-  let
-    val sort_of = sort_of_term;
+(* decode_typ *)
 
-    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
-          insert (op =) ((x, ~1), sort_of cs)
-      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
-          insert (op =) ((x, ~1), sort_of cs)
-      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
-          insert (op =) (xi, sort_of cs)
-      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
-          insert (op =) (xi, sort_of cs)
-      | add_env (Abs (_, _, t)) = add_env t
-      | add_env (t1 $ t2) = add_env t1 #> add_env t2
-      | add_env _ = I;
-  in add_env tm [] end;
+fun decode_typ tm =
+  let
+    fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
 
-
-(* typ_of_term *)
-
-fun typ_of_term get_sort tm =
-  let
-    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
-
-    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
-      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
-      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
-      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
-      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
-      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
-          TFree (x, get_sort (x, ~1))
-      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
-      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
-          TVar (xi, get_sort xi)
-      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
-      | typ_of t =
+    fun typ (Free (x, _)) = TFree (x, dummyS)
+      | typ (Var (xi, _)) = TVar (xi, dummyS)
+      | typ (Const ("_tfree",_) $ (t as Free _)) = typ t
+      | typ (Const ("_tvar",_) $ (t as Var _)) = typ t
+      | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s)
+      | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) =
+          TFree (x, decode_sort s)
+      | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s)
+      | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) =
+          TVar (xi, decode_sort s)
+      | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s)
+      | typ t =
           let
             val (head, args) = Term.strip_comb t;
             val a =
               (case head of
                 Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
               | _ => err ());
-          in Type (a, map typ_of args) end;
-  in typ_of tm end;
+          in Type (a, map typ args) end;
+  in typ tm end;
 
 
 (* parsetree_to_ast *)
@@ -207,19 +187,17 @@
             handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
         val get_free = Proof_Context.intern_skolem ctxt;
 
-        val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
-
         val reports = Unsynchronized.ref reports0;
         fun report ps = Position.store_reports reports ps;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME p => decode (p :: ps) qs bs t
-              | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
+              | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME q => decode ps (q :: qs) bs t
-              | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
+              | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
               let
                 val id = serial ();
@@ -328,7 +306,7 @@
     (fn (syms, pos) =>
       parse_raw ctxt "sort" (syms, pos)
       |> report_result ctxt pos
-      |> sort_of_term
+      |> decode_sort
       |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
@@ -337,7 +315,7 @@
     (fn (syms, pos) =>
       parse_raw ctxt "type" (syms, pos)
       |> report_result ctxt pos
-      |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
+      |> decode_typ
       handle ERROR msg => parse_failed ctxt pos msg "type");
 
 fun parse_term is_prop ctxt =
@@ -714,11 +692,31 @@
 
 (** check/uncheck **)
 
+fun prepare_types ctxt tys =
+  let
+    fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
+    val env =
+      (fold o fold_atyps)
+        (fn TFree (x, S) => constraint ((x, ~1), S)
+          | TVar v => constraint v
+          | _ => I) tys [];
+    val get_sort = Proof_Context.get_sort ctxt env;
+  in
+    (map o map_atyps)
+      (fn TFree (x, _) => TFree (x, get_sort (x, ~1))
+        | TVar (xi, _) => TVar (xi, get_sort xi)
+        | T => T) tys
+  end;
+
 fun check_typs ctxt =
-  Syntax.apply_typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt);
+  prepare_types ctxt #>
+  Syntax.apply_typ_check ctxt #>
+  Term_Sharing.typs (Proof_Context.theory_of ctxt);
 
 fun check_terms ctxt =
-  Syntax.apply_term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt);
+  Term.burrow_types (prepare_types ctxt) #>
+  Syntax.apply_term_check ctxt #>
+  Term_Sharing.terms (Proof_Context.theory_of ctxt);
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 

--- a/src/Pure/sign.ML	Wed Nov 09 17:12:26 2011 +0100
+++ b/src/Pure/sign.ML	Wed Nov 09 17:57:42 2011 +0100
@@ -361,18 +361,18 @@
 
 fun gen_syntax change_gram parse_typ mode args thy =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
 
 fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
 
-val add_modesyntax = gen_add_syntax Syntax.parse_typ;
+val add_modesyntax = gen_add_syntax Syntax.read_typ;
 val add_modesyntax_i = gen_add_syntax (K I);
 val add_syntax = add_modesyntax Syntax.mode_default;
 val add_syntax_i = add_modesyntax_i Syntax.mode_default;
-val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
+val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
 val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
 
 fun type_notation add mode args =
@@ -396,9 +396,9 @@
 
 local
 
-fun gen_add_consts parse_typ ctxt raw_args thy =
+fun gen_add_consts prep_typ ctxt raw_args thy =
   let
-    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
+    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt;
     fun prep (b, raw_T, mx) =
       let
         val c = full_name thy b;
@@ -417,7 +417,8 @@
 in
 
 fun add_consts args thy =
-  #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy);
+  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
+
 fun add_consts_i args thy =
   #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);