# HG changeset patch
# User huffman
# Date 1320932798 -3600
# Node ID 34de78f802aaf8eaee28db6879db497750c64307
# Parent  1006cba234e3be5682a8bfe4e3c5c473d7cc0eb9# Parent  f28329338d30579b34f703d7271365f9d687a8c9
merged

diff -r 1006cba234e3 -r 34de78f802aa NEWS
--- a/NEWS	Wed Nov 09 15:33:34 2011 +0100
+++ b/NEWS	Thu Nov 10 14:46:38 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 ***
 
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Thu Nov 10 14:46:38 2011 +0100
@@ -15,31 +15,35 @@
   "x \<notin> S \<Longrightarrow> indicator S x = 0"
   unfolding indicator_def by auto
 
-lemma
-  shows indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
+lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
   and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
-  and indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
+  unfolding indicator_def by auto
+
+lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
   unfolding indicator_def by auto
 
 lemma split_indicator:
   "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
   unfolding indicator_def by auto
 
-lemma
-  shows indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
-  and indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
-  and indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
+lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
   and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
-  and indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
   and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
   unfolding indicator_def by (auto simp: min_def max_def)
 
-lemma
-  shows indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
+lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
   unfolding indicator_def by (cases x) auto
 
-lemma
-  shows indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
+lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
   unfolding indicator_def by (cases x) auto
 
 lemma
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -496,7 +496,8 @@
     val ctxt' = Proof_Context.init_global thy
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
-    val test = Quickcheck_Common.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
+    val test = Quickcheck_Common.test_term
+      ("exhaustive", Exhaustive_Generators.compile_generator_expr) ctxt' false
   in  
     case try test (preprocess thy insts (prop_of th), []) of
       SOME _ => (Output.urgent_message "executable"; true)
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -123,7 +123,7 @@
             val ctxt' = change_options (Proof_Context.init_global thy)
             val [result] = case Quickcheck.active_testers ctxt' of
               [] => error "No active testers for quickcheck"
-            | [tester] => tester ctxt' (false, false) [] [(t, [])]
+            | [tester] => tester ctxt' false [] [(t, [])]
             | _ => error "Multiple active testers for quickcheck"
           in
             case Quickcheck.counterexample_of result of 
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Presburger.thy	Thu Nov 10 14:46:38 2011 +0100
@@ -25,8 +25,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x<z. F = F"
   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all
 
@@ -41,8 +41,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x>z. F = F"
   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all
 
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -136,9 +136,10 @@
         (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
     
     val tycos = map fst dataTs;
-    val _ = if eq_set (op =) (tycos, raw_tycos) then ()
-      else error ("Type constructors " ^ commas (map quote raw_tycos)
-        ^ " do not belong exhaustively to one mutual recursive datatype");
+    val _ =
+      if eq_set (op =) (tycos, raw_tycos) then ()
+      else error ("Type constructors " ^ commas_quote raw_tycos ^
+        " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;
 
@@ -406,15 +407,16 @@
       in (tyco, (vs, cT)) end;
 
     val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
-    val _ = case map_filter (fn (tyco, _) =>
-        if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
-     of [] => ()
-      | tycos => error ("Type(s) " ^ commas (map quote tycos)
-          ^ " already represented inductivly");
+    val _ =
+      (case map_filter (fn (tyco, _) =>
+          if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs of
+        [] => ()
+      | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly"));
     val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
-    val ms = case distinct (op =) (map length raw_vss)
-     of [n] => 0 upto n - 1
-      | _ => error ("Different types in given constructors");
+    val ms =
+      (case distinct (op =) (map length raw_vss) of
+         [n] => 0 upto n - 1
+      | _ => error "Different types in given constructors");
     fun inter_sort m = map (fn xs => nth xs m) raw_vss
       |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
     val sorts = map inter_sort ms;
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -224,7 +224,7 @@
   #> Code.abstype_interpretation ensure_term_of
   #> Code.datatype_interpretation ensure_term_of_code
   #> Code.abstype_interpretation ensure_abs_term_of_code
-  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
   #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
 
 end;
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Tools/record.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -249,9 +249,7 @@
 
 (*** utilities ***)
 
-fun varifyT midx =
-  let fun varify (a, S) = TVar ((a, midx + 1), S);
-  in map_type_tfree varify end;
+fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
 
 
 (* timing *)
@@ -582,8 +580,7 @@
     val recname =
       let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
       in Long_Name.implode (rev (nm :: rst)) end;
-    val midx = maxidx_of_typs (moreT :: Ts);
-    val varifyT = varifyT midx;
+    val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
     val {records, extfields, ...} = Data.get thy;
     val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
@@ -655,17 +652,6 @@
 
 (** concrete syntax for records **)
 
-(* decode type *)
-
-fun decode_type thy t =
-  let
-    fun get_sort env xi =
-      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
-  in
-    Syntax_Phases.typ_of_term (get_sort (Syntax_Phases.term_sorts t)) t
-  end;
-
-
 (* parse translations *)
 
 local
@@ -702,9 +688,8 @@
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs
                       handle Fail msg => err msg;
-                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
-                    val midx = fold Term.maxidx_typ argtypes 0;
-                    val varifyT = varifyT midx;
+                    val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
+                    val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
                     val vartypes = map varifyT types;
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
@@ -808,8 +793,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val T = decode_type thy t;
-    val varifyT = varifyT (Term.maxidx_of_typ T);
+    val T = Syntax_Phases.decode_typ t;
+    val varifyT = varifyT (Term.maxidx_of_typ T + 1);
 
     fun strip_fields T =
       (case T of
@@ -853,10 +838,8 @@
   the (nested) extension types*)
 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val T = decode_type thy tm;
-    val midx = maxidx_of_typ T;
-    val varifyT = varifyT midx;
+    val T = Syntax_Phases.decode_typ tm;
+    val varifyT = varifyT (maxidx_of_typ T + 1);
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
diff -r 1006cba234e3 -r 34de78f802aa src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/HOL/Tools/transfer.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -77,7 +77,7 @@
   let
     val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints
       then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context);
-    val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else ();
+    val _ = if null insts then error ("Transfer: no such labels: " ^ commas_quote hints) else ();
   in insts end;
 
 fun splits P [] = []
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Isar/class.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -550,7 +550,7 @@
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.activate_improvable_syntax
-    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
+    |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
     |> Local_Theory.init NONE ""
        {define = Generic_Target.define foundation,
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -41,7 +41,8 @@
     val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
            Expression.Named param_map_const))], []);
-    val (props, inst_morph) = if null param_map
+    val (props, inst_morph) =
+      if null param_map
       then (raw_props |> map (Morphism.term typ_morph),
         raw_inst_morph $> typ_morph)
       else (raw_props, raw_inst_morph); (*FIXME proper handling in
@@ -49,13 +50,15 @@
 
     (* witness for canonical interpretation *)
     val prop = try the_single props;
-    val wit = Option.map (fn prop => let
+    val wit = Option.map (fn prop =>
+      let
         val sup_axioms = map_filter (fst o Class.rules thy) sups;
-        val loc_intro_tac = case Locale.intros_of thy class
-          of (_, NONE) => all_tac
-           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
+        val loc_intro_tac =
+          (case Locale.intros_of thy class of
+            (_, NONE) => all_tac
+          | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
         val tac = loc_intro_tac
-          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom))
+          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
       in Element.prove_witness empty_ctxt prop tac end) prop;
     val axiom = Option.map Element.conclude_witness wit;
 
@@ -69,9 +72,10 @@
     fun prove_assm_intro thm =
       let
         val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
-        val const_eq_morph = case eq_morph
-         of SOME eq_morph => const_morph $> eq_morph
-          | NONE => const_morph
+        val const_eq_morph =
+          (case eq_morph of
+             SOME eq_morph => const_morph $> eq_morph
+          | NONE => const_morph);
         val thm'' = Morphism.thm const_eq_morph thm';
         val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
       in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
@@ -80,17 +84,19 @@
 
     (* of_class *)
     val of_class_prop_concl = Logic.mk_of_class (aT, class);
-    val of_class_prop = case prop of NONE => of_class_prop_concl
+    val of_class_prop =
+      (case prop of
+        NONE => of_class_prop_concl
       | SOME prop => Logic.mk_implies (Morphism.term const_morph
-          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
+          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
     val sup_of_classes = map (snd o Class.rules thy) sups;
     val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     val axclass_intro = #intro (AxClass.get_info thy class);
     val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
-    val tac = REPEAT (SOMEGOAL
-      (Tactic.match_tac (axclass_intro :: sup_of_classes
-         @ loc_axiom_intros @ base_sort_trivs)
-           ORELSE' Tactic.assume_tac));
+    val tac =
+      REPEAT (SOMEGOAL
+        (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
+          ORELSE' Tactic.assume_tac));
     val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
 
   in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
@@ -104,40 +110,45 @@
     (* user space type system: only permits 'a type variable, improves towards 'a *)
     val algebra = Sign.classes_of thy;
     val inter_sort = curry (Sorts.inter_sort algebra);
-    val proto_base_sort = if null sups then Sign.defaultS thy
+    val proto_base_sort =
+      if null sups then Sign.defaultS thy
       else fold inter_sort (map (Class.base_sort thy) sups) [];
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
         (Class.these_operations thy sups);
-    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
-          if v = Name.aT then T
-          else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
-      | T => T);
-    fun singleton_fixate Ts =
+    fun singleton_fixate tms =
       let
-        fun extract f = (fold o fold_atyps) f Ts [];
-        val tfrees = extract
-          (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
-        val inferred_sort = extract
-          (fn TVar (_, sort) => inter_sort sort | _ => I);
-        val fixate_sort = if null tfrees then inferred_sort
-          else case tfrees
-           of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
-                then inter_sort a_sort inferred_sort
-                else error ("Type inference imposes additional sort constraint "
-                  ^ Syntax.string_of_sort_global thy inferred_sort
-                  ^ " of type parameter " ^ Name.aT ^ " of sort "
-                  ^ Syntax.string_of_sort_global thy a_sort)
-            | _ => error "Multiple type variables in class specification";
-      in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
-    fun after_infer_fixate Ts =
+        val tfrees = fold Term.add_tfrees tms [];
+        val inferred_sort =
+          (fold o fold_types o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) tms [];
+        val fixate_sort =
+          (case tfrees of
+            [] => inferred_sort
+          | [(a, S)] =>
+              if a <> Name.aT then
+                error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
+              else if Sorts.sort_le algebra (S, inferred_sort) then S
+              else
+                error ("Type inference imposes additional sort constraint " ^
+                  Syntax.string_of_sort_global thy inferred_sort ^
+                  " of type parameter " ^ Name.aT ^ " of sort " ^
+                  Syntax.string_of_sort_global thy S)
+          | _ => error "Multiple type variables in class specification");
+        val fixateT = TFree (Name.aT, fixate_sort);
+      in
+        (map o map_types o map_atyps)
+          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) tms
+      end;
+    fun after_infer_fixate tms =
       let
-        val sort' = (fold o fold_atyps) (fn T as TFree _ => I | T as TVar (vi, sort) =>
-          if Type_Infer.is_param vi then inter_sort sort else I) Ts [];
+        val fixate_sort =
+          (fold o fold_types o fold_atyps)
+            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) tms [];
       in
-        (map o map_atyps)
-          (fn T as TFree _ => T | T as TVar (vi, _) =>
-            if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
+        (map o map_types o map_atyps)
+          (fn T as TVar (xi, _) =>
+              if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, fixate_sort) else T
+            | T => T) tms
       end;
 
     (* preprocessing elements, retrieving base sort from type-checked elements *)
@@ -146,11 +157,10 @@
     val init_class_body =
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
-      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
+      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems), _) =
       Proof_Context.init_global thy
-      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
+      |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e
@@ -158,18 +168,22 @@
       | filter_element (e as Element.Constrains _) = SOME e
       | filter_element (Element.Assumes []) = NONE
       | filter_element (e as Element.Assumes _) = SOME e
-      | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.")
-      | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.");
+      | filter_element (Element.Defines _) =
+          error ("\"defines\" element not allowed in class specification.")
+      | filter_element (Element.Notes _) =
+          error ("\"notes\" element not allowed in class specification.");
     val inferred_elems = map_filter filter_element raw_inferred_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
           fold_types f t #> (fold o fold_types) f ts) o snd) assms;
-    val base_sort = if null inferred_elems then proto_base_sort else
-      case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
-       of [] => error "No type variable in class specification"
+    val base_sort =
+      if null inferred_elems then proto_base_sort
+      else
+        (case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of
+          [] => error "No type variable in class specification"
         | [(_, sort)] => sort
-        | _ => error "Multiple type variables in class specification";
+        | _ => error "Multiple type variables in class specification");
     val supparams = map (fn ((c, T), _) =>
       (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
     val supparam_names = map fst supparams;
@@ -188,38 +202,39 @@
 
     (* prepare import *)
     val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val sups = map (prep_class thy) raw_supclasses
-      |> Sign.minimize_sort thy;
-    val _ = case filter_out (Class.is_class thy) sups
-     of [] => ()
-      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
+    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
+    val _ =
+      (case filter_out (Class.is_class thy) sups of
+        [] => ()
+      | no_classes => error ("No (proper) classes: " ^ commas_quote no_classes));
     val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups);
     val raw_supparam_names = map fst raw_supparams;
-    val _ = if has_duplicates (op =) raw_supparam_names
-      then error ("Duplicate parameter(s) in superclasses: "
-        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
+    val _ =
+      if has_duplicates (op =) raw_supparam_names then
+        error ("Duplicate parameter(s) in superclasses: " ^
+          (commas_quote (duplicates (op =) raw_supparam_names)))
       else ();
 
     (* infer types and base sort *)
-    val (base_sort, supparam_names, supexpr, inferred_elems) =
-      prep_class_elems thy sups raw_elems;
+    val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems;
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
     val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
-    fun check_vars e vs = if null vs
-      then error ("No type variable in part of specification element "
-        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
+    fun check_vars e vs =
+      if null vs then
+        error ("No type variable in part of specification element " ^
+          Pretty.string_of (Pretty.chunks (Element.pretty_ctxt class_ctxt e)))
       else ();
     fun check_element (e as Element.Fixes fxs) =
-          map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
+          List.app (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
       | check_element (e as Element.Assumes assms) =
-          maps (fn (_, ts_pss) => map
-            (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
-      | check_element e = [()];
-    val _ = map check_element syntax_elems;
+          List.app (fn (_, ts_pss) =>
+            List.app (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
+      | check_element _ = ();
+    val _ = List.app check_element syntax_elems;
     fun fork_syn (Element.Fixes xs) =
           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
@@ -273,9 +288,10 @@
     val raw_pred = Locale.intros_of thy class
       |> fst
       |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
-    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
-     of [] => NONE
-      | [thm] => SOME thm;
+    fun get_axiom thy =
+      (case #axioms (AxClass.get_info thy class) of
+         [] => NONE
+      | [thm] => SOME thm);
   in
     thy
     |> add_consts class base_sort sups supparam_names global_syntax
@@ -317,6 +333,7 @@
 end; (*local*)
 
 
+
 (** subclass relations **)
 
 local
@@ -325,9 +342,10 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case Named_Target.peek lthy
-     of SOME {target, is_class = true, ...} => target
-      | _ => error "Not in a class target";
+    val proto_sub =
+      (case Named_Target.peek lthy of
+         SOME {target, is_class = true, ...} => target
+      | _ => error "Not in a class target");
     val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
 
     val expr = ([(sup, (("", false), Expression.Positional []))], []);
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Isar/code.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -1174,7 +1174,7 @@
     val (case_const, (k, cos)) = case_cert thm;
     val _ = case filter_out (is_constr thy) cos
      of [] => ()
-      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+      | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
     val entry = (1 + Int.max (1, length cos), (k, cos));
     fun register_case cong = (map_cases o apfst)
       (Symtab.update (case_const, (entry, cong)));
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -114,8 +114,8 @@
 
 val activate_improvable_syntax =
   Context.proof_map
-    (Syntax.context_term_check 0 "improvement" improve_term_check
-    #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
+    (Syntax_Phases.context_term_check 0 "improvement" improve_term_check
+    #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck)
   #> set_primary_constraints;
 
 
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 10 14:46:38 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
@@ -84,6 +83,9 @@
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
   val def_type: Proof.context -> indexname -> typ option
+  val standard_typ_check: Proof.context -> typ list -> typ list
+  val standard_term_check_finish: Proof.context -> term list -> term list
+  val standard_term_uncheck: Proof.context -> term list -> term list
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
@@ -639,8 +641,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 *)
@@ -668,23 +669,12 @@
   let val Mode {pattern, ...} = get_mode ctxt
   in Variable.def_type ctxt pattern end;
 
-local
-
 fun standard_typ_check ctxt =
-  map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
-  map (prepare_patternT ctxt);
-
-fun standard_term_uncheck ctxt =
-  map (contract_abbrevs ctxt);
+  map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt);
 
-in
+val standard_term_check_finish = prepare_patterns;
 
-val _ = Context.>>
- (Syntax.add_typ_check 0 "standard" standard_typ_check #>
-  Syntax.add_term_check 100 "fixate" prepare_patterns #>
-  Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
-
-end;
+fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt);
 
 
 
@@ -940,7 +930,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;
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -30,31 +30,6 @@
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
-  val print_checks: Proof.context -> unit
-  val context_typ_check: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_check: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_typ_uncheck: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_uncheck: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val typ_check: Proof.context -> typ list -> typ list
-  val term_check: Proof.context -> term list -> term list
-  val typ_uncheck: Proof.context -> typ list -> typ list
-  val term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -244,88 +219,7 @@
 val unparse_term = operation #unparse_term;
 
 
-(* context-sensitive (un)checking *)
-
-type key = int * bool;
-
-structure Checks = Generic_Data
-(
-  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
-  type T =
-    ((key * ((string * typ check) * stamp) list) list *
-     (key * ((string * term check) * stamp) list) list);
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
-    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
-     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
-);
-
-fun print_checks ctxt =
-  let
-    fun split_checks checks =
-      List.partition (fn ((_, un), _) => not un) checks
-      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
-          #> sort (int_ord o pairself fst));
-    fun pretty_checks kind checks =
-      checks |> map (fn (i, names) => Pretty.block
-        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
-          Pretty.brk 1, Pretty.strs names]);
-
-    val (typs, terms) = Checks.get (Context.Proof ctxt);
-    val (typ_checks, typ_unchecks) = split_checks typs;
-    val (term_checks, term_unchecks) = split_checks terms;
-  in
-    pretty_checks "typ_checks" typ_checks @
-    pretty_checks "term_checks" term_checks @
-    pretty_checks "typ_unchecks" typ_unchecks @
-    pretty_checks "term_unchecks" term_unchecks
-  end |> Pretty.chunks |> Pretty.writeln;
-
-
-local
-
-fun context_check which (key: key) name f =
-  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
-
-fun simple_check eq f xs ctxt =
-  let val xs' = f ctxt xs
-  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
-
-in
-
-fun context_typ_check stage = context_check apfst (stage, false);
-fun context_term_check stage = context_check apsnd (stage, false);
-fun context_typ_uncheck stage = context_check apfst (stage, true);
-fun context_term_uncheck stage = context_check apsnd (stage, true);
-
-fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
-fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
-fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
-fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
-
-end;
-
-
-local
-
-fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
-fun check_all fs = perhaps_apply (map check_stage fs);
-
-fun check which uncheck ctxt0 xs0 =
-  let
-    val funs = which (Checks.get (Context.Proof ctxt0))
-      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
-      |> Library.sort (int_ord o pairself fst) |> map snd
-      |> not uncheck ? map rev;
-  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
-
-in
-
-val typ_check = check fst false;
-val term_check = check snd false;
-val typ_uncheck = check fst true;
-val term_uncheck = check snd true;
+(* (un)checking *)
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
@@ -338,8 +232,6 @@
 val uncheck_typs = operation #uncheck_typs;
 val uncheck_terms = operation #uncheck_terms;
 
-end;
-
 
 (* derived operations for algebra of sorts *)
 
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -7,12 +7,33 @@
 
 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
   val term_of_typ: Proof.context -> typ -> term
+  val print_checks: Proof.context -> unit
+  val context_typ_check: int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_term_check: int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_typ_uncheck: int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_term_uncheck: int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
+    Context.generic -> Context.generic
+  val term_check: int -> string -> (Proof.context -> term list -> term list) ->
+    Context.generic -> Context.generic
+  val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
+    Context.generic -> Context.generic
+  val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
+    Context.generic -> Context.generic
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
@@ -58,11 +79,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 +98,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 +208,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 +327,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 +336,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,12 +713,131 @@
 
 (** check/uncheck **)
 
-fun check_typs ctxt = Syntax.typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt);
-fun check_terms ctxt = Syntax.term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt);
+(* context-sensitive (un)checking *)
+
+type key = int * bool;
+
+structure Checks = Generic_Data
+(
+  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
+  type T =
+    ((key * ((string * typ check) * stamp) list) list *
+     (key * ((string * term check) * stamp) list) list);
+  val empty = ([], []);
+  val extend = I;
+  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
+    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
+     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
+);
+
+fun print_checks ctxt =
+  let
+    fun split_checks checks =
+      List.partition (fn ((_, un), _) => not un) checks
+      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
+          #> sort (int_ord o pairself fst));
+    fun pretty_checks kind checks =
+      checks |> map (fn (i, names) => Pretty.block
+        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
+          Pretty.brk 1, Pretty.strs names]);
+
+    val (typs, terms) = Checks.get (Context.Proof ctxt);
+    val (typ_checks, typ_unchecks) = split_checks typs;
+    val (term_checks, term_unchecks) = split_checks terms;
+  in
+    pretty_checks "typ_checks" typ_checks @
+    pretty_checks "term_checks" term_checks @
+    pretty_checks "typ_unchecks" typ_unchecks @
+    pretty_checks "term_unchecks" term_unchecks
+  end |> Pretty.chunks |> Pretty.writeln;
+
+
+local
+
+fun context_check which (key: key) name f =
+  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
+
+fun simple_check eq f xs ctxt =
+  let val xs' = f ctxt xs
+  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
+
+in
+
+fun context_typ_check stage = context_check apfst (stage, false);
+fun context_term_check stage = context_check apsnd (stage, false);
+fun context_typ_uncheck stage = context_check apfst (stage, true);
+fun context_term_uncheck stage = context_check apsnd (stage, true);
+
+fun typ_check key name f = context_typ_check key name (simple_check (op =) f);
+fun term_check key name f = context_term_check key name (simple_check (op aconv) f);
+fun typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
+fun term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
+
+end;
+
+
+local
+
+fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
+fun check_all fs = perhaps_apply (map check_stage fs);
+
+fun check which uncheck ctxt0 xs0 =
+  let
+    val funs = which (Checks.get (Context.Proof ctxt0))
+      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
+      |> Library.sort (int_ord o pairself fst) |> map snd
+      |> not uncheck ? map rev;
+  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
+
+val apply_typ_check = check fst false;
+val apply_term_check = check snd false;
+val apply_typ_uncheck = check fst true;
+val apply_term_uncheck = check snd true;
+
+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;
+
+in
+
+fun check_typs ctxt =
+  prepare_types ctxt #>
+  apply_typ_check ctxt #>
+  Term_Sharing.typs (Proof_Context.theory_of ctxt);
+
+fun check_terms ctxt =
+  Term.burrow_types (prepare_types ctxt) #>
+  apply_term_check ctxt #>
+  Term_Sharing.terms (Proof_Context.theory_of ctxt);
+
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
-val uncheck_typs = Syntax.typ_uncheck;
-val uncheck_terms = Syntax.term_uncheck;
+val uncheck_typs = apply_typ_uncheck;
+val uncheck_terms = apply_term_uncheck;
+
+end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (typ_check 0 "standard" Proof_Context.standard_typ_check #>
+  term_check 0 "standard"
+    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
 
 
 
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/sign.ML	Thu Nov 10 14:46:38 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);
 
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/type_infer_context.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -259,9 +259,4 @@
     val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
   in ts' end;
 
-val _ =
-  Context.>>
-    (Syntax.add_term_check 0 "standard"
-      (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
-
 end;
diff -r 1006cba234e3 -r 34de78f802aa src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Pure/variable.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -223,10 +223,10 @@
       (fn Free (x, T) => Vartab.update ((x, ~1), T)
         | Var v => Vartab.update v
         | _ => I) t types;
-    val sorts' = fold_types (fold_atyps
+    val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
         | TVar v => constrain_tvar v
-        | _ => I)) t sorts;
+        | _ => I) t sorts;
   in (types', sorts') end)
   #> declare_type_occsT t
   #> declare_type_names t;
diff -r 1006cba234e3 -r 34de78f802aa src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -264,11 +264,11 @@
           let
             val missing_constrs = subtract (op =) consts constrs;
             val _ = if null missing_constrs then []
-              else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+              else error ("Missing constructor(s) " ^ commas_quote missing_constrs
                 ^ " for datatype " ^ quote tyco);
             val false_constrs = subtract (op =) constrs consts;
             val _ = if null false_constrs then []
-              else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+              else error ("Non-constructor(s) " ^ commas_quote false_constrs
                 ^ " for datatype " ^ quote tyco)
           in () end
       | NONE => ();
diff -r 1006cba234e3 -r 34de78f802aa src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -6,20 +6,17 @@
 
 signature ADHOC_OVERLOADING =
 sig
-
   val add_overloaded: string -> theory -> theory
   val add_variant: string -> string -> theory -> theory
 
-  val show_variants: bool Unsynchronized.ref
+  val show_variants: bool Config.T
   val setup: theory -> theory
-
 end
 
-
 structure Adhoc_Overloading: ADHOC_OVERLOADING =
 struct
 
-val show_variants = Unsynchronized.ref false;
+val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
 
 
 (* errors *)
@@ -75,13 +72,14 @@
 fun add_variant ext_name name thy =
   let
     val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
-    val _ = case get_external thy name of
-              NONE => ()
-            | SOME gen' => duplicate_variant_err name gen';
+    val _ =
+      (case get_external thy name of
+        NONE => ()
+      | SOME gen' => duplicate_variant_err name gen');
     val T = Sign.the_const_type thy name;
   in
     map_tables (Symtab.cons_list (ext_name, (name, T)))
-      (Symtab.update (name, ext_name)) thy    
+      (Symtab.update (name, ext_name)) thy
   end
 
 
@@ -99,15 +97,15 @@
   end;
 
 fun insert_internal_same ctxt t (Const (c, T)) =
-  (case map_filter (unifiable_with ctxt T) 
-     (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of
-      [] => unresolved_err ctxt (c, T) t "no instances"
-    | [c'] => Const (c', dummyT)
-    | _ => raise Same.SAME)
+      (case map_filter (unifiable_with ctxt T)
+         (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of
+        [] => unresolved_err ctxt (c, T) t "no instances"
+      | [c'] => Const (c', dummyT)
+      | _ => raise Same.SAME)
   | insert_internal_same _ _ _ = raise Same.SAME;
 
 fun insert_external_same ctxt _ (Const (c, T)) =
-    Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T)
+      Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T)
   | insert_external_same _ _ _ = raise Same.SAME;
 
 fun gen_check_uncheck replace ts ctxt =
@@ -115,27 +113,27 @@
   |> Option.map (rpair ctxt);
 
 val check = gen_check_uncheck insert_internal_same;
-fun uncheck ts ctxt = 
-  if !show_variants then NONE
+
+fun uncheck ts ctxt =
+  if Config.get ctxt show_variants then NONE
   else gen_check_uncheck insert_external_same ts ctxt;
 
 fun reject_unresolved ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun check_unresolved t =
-      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
-          [] => ()
-        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
-
+      (case filter (is_overloaded thy o fst) (Term.add_consts t []) of
+        [] => ()
+      | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances");
     val _ = map check_unresolved ts;
   in NONE end;
 
 
 (* setup *)
 
-val setup = Context.theory_map 
-  (Syntax.context_term_check 0 "adhoc_overloading" check
-   #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
-   #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck);
+val setup = Context.theory_map
+  (Syntax_Phases.context_term_check 0 "adhoc_overloading" check
+   #> Syntax_Phases.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+   #> Syntax_Phases.context_term_uncheck 0 "adhoc_overloading" uncheck);
 
-end
+end;
diff -r 1006cba234e3 -r 34de78f802aa src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Nov 09 15:33:34 2011 +0100
+++ b/src/Tools/subtyping.ML	Thu Nov 10 14:46:38 2011 +0100
@@ -806,7 +806,7 @@
 val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
 
 val add_term_check =
-  Syntax.add_term_check ~100 "coercions"
+  Syntax_Phases.term_check ~100 "coercions"
     (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);