simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;

--- a/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -150,8 +150,8 @@
       | NONE => NONE)
   | subst_termify t = subst_termify_app (strip_comb t) 
 
-fun check_termify ts ctxt = map_default subst_termify ts
-  |> Option.map (rpair ctxt)
+fun check_termify ctxt ts =
+  the_default ts (map_default subst_termify ts);
 
 
 (** evaluation **)

--- a/src/Pure/Isar/class.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Isar/class.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -462,7 +462,7 @@
       handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
     val inst = map_type_tvar
       (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
-  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
+  in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
 
 
 (* target *)
@@ -535,10 +535,7 @@
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
       (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
-    fun resort_check ts ctxt =
-      (case resort_terms ctxt algebra consts improve_constraints ts of
-        NONE => NONE
-      | SOME ts' => SOME (ts', ctxt));
+    fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
     val lookup_inst_param = AxClass.lookup_inst_param consts params;
     fun improve (c, ty) =
       (case lookup_inst_param (c, ty) of

--- a/src/Pure/Isar/class_declaration.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -139,19 +139,18 @@
           (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
       end;
-    fun add_typ_check level name f = Context.proof_map
-      (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
-        let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
 
     (* preprocessing elements, retrieving base sort from type-checked elements *)
-    val raw_supexpr = (map (fn sup => (sup, (("", false),
-      Expression.Positional []))) sups, []);
-    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
+    val raw_supexpr =
+      (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
+    val init_class_body =
+      fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
-      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
-    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
-      |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
+      #> 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));
+    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))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e
@@ -165,7 +164,7 @@
     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
+          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"

--- a/src/Pure/Isar/overloading.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -113,8 +113,8 @@
 
 val activate_improvable_syntax =
   Context.proof_map
-    (Syntax.add_term_check 0 "improvement" improve_term_check
-    #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
+    (Syntax.context_term_check 0 "improvement" improve_term_check
+    #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
   #> set_primary_constraints;
 
 

--- a/src/Pure/Isar/proof_context.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -700,16 +700,13 @@
 fun standard_term_uncheck ctxt =
   map (contract_abbrevs ctxt);
 
-fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
-  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
-
 in
 
-val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check;
-val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check;
-val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns;
-
-val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
+val _ = Context.>>
+ (Syntax.add_typ_check 0 "standard" standard_typ_check #>
+  Syntax.add_term_check 0 "standard" standard_term_check #>
+  Syntax.add_term_check 100 "fixate" prepare_patterns #>
+  Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
 
 end;
 

--- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -31,18 +31,26 @@
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
   val print_checks: Proof.context -> unit
-  val add_typ_check: int -> string ->
+  val context_typ_check: int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
-  val add_term_check: int -> string ->
+  val context_term_check: int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
-  val add_typ_uncheck: int -> string ->
+  val context_typ_uncheck: int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
-  val add_term_uncheck: int -> string ->
+  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
@@ -224,13 +232,11 @@
 
 (* context-sensitive (un)checking *)
 
-local
-
 type key = int * bool;
-type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
 
 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);
@@ -241,27 +247,6 @@
      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
 );
 
-fun gen_add which (key: key) name f =
-  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
-
-fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
-
-fun gen_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;
-    val check_all = perhaps_apply (map check_stage funs);
-  in #1 (perhaps check_all (xs0, ctxt0)) end;
-
-fun map_sort f S =
-  (case f (TFree ("", S)) of
-    TFree ("", S') => S'
-  | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
-
-in
-
 fun print_checks ctxt =
   let
     fun split_checks checks =
@@ -283,15 +268,52 @@
     pretty_checks "term_unchecks" term_unchecks
   end |> Pretty.chunks |> Pretty.writeln;
 
-fun add_typ_check stage = gen_add apfst (stage, false);
-fun add_term_check stage = gen_add apsnd (stage, false);
-fun add_typ_uncheck stage = gen_add apfst (stage, true);
-fun add_term_uncheck stage = gen_add apsnd (stage, true);
+
+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 pointer_eq (xs, xs') orelse 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);
 
-val typ_check = gen_check fst false;
-val term_check = gen_check snd false;
-val typ_uncheck = gen_check fst true;
-val term_uncheck = gen_check snd 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;
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
@@ -300,17 +322,30 @@
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;
 val check_prop = singleton o check_props;
-val check_sort = map_sort o check_typ;
 
 val uncheck_typs = operation #uncheck_typs;
 val uncheck_terms = operation #uncheck_terms;
+
+end;
+
+
+(* derived operations for algebra of sorts *)
+
+local
+
+fun map_sort f S =
+  (case f (TFree ("", S)) of
+    TFree ("", S') => S'
+  | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
+
+in
+
+val check_sort = map_sort o check_typ;
 val uncheck_sort = map_sort o singleton o uncheck_typs;
 
 end;
 
 
-(* derived operations for classrel and arity *)
-
 val uncheck_classrel = map o singleton o uncheck_sort;
 
 fun unparse_classrel ctxt cs = Pretty.block (flat

--- a/src/Tools/adhoc_overloading.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Tools/adhoc_overloading.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -134,8 +134,8 @@
 (* setup *)
 
 val setup = Context.theory_map 
-  (Syntax.add_term_check 0 "adhoc_overloading" check
-   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
-   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
+  (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);
 
 end

--- a/src/Tools/subtyping.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Tools/subtyping.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -713,15 +713,12 @@
 
 (* term check *)
 
-val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
+val (coercion_enabled, coercion_enabled_setup) =
+  Attrib.config_bool "coercion_enabled" (K false);
 
 val add_term_check =
   Syntax.add_term_check ~100 "coercions"
-    (fn xs => fn ctxt =>
-      if Config.get ctxt coercion_enabled then
-        let val xs' = coercion_infer_types ctxt xs
-        in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
-      else NONE);
+    (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
 
 
 (* declarations *)