Syntax.(un)check: explicit result option;

--- a/src/Pure/Isar/class.ML	Tue Oct 16 19:45:56 2007 +0200
+++ b/src/Pure/Isar/class.ML	Tue Oct 16 19:45:57 2007 +0200
@@ -18,7 +18,7 @@
     -> string list -> theory -> string * Proof.context
   val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
-  val init: class -> Proof.context -> Proof.context;
+  val init: class -> Proof.context -> Proof.context
   val add_const_in_class: string -> (string * mixfix) * (string * term)
     -> theory -> string * theory
   val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
@@ -588,7 +588,7 @@
       #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
            then TFree (Name.aT, local_sort) else TVar var)) ts;
     val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
-  in (ts', ctxt') end;
+  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
 
 val uncheck = ref false;
 
@@ -605,7 +605,7 @@
           | NONE => t)
       | globalize t = t;
     val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
-  in (ts', ctxt) end;
+  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
 
 fun init_class_ctxt sups local_sort ctxt =
   let

--- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:56 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:57 2007 +0200
@@ -585,16 +585,17 @@
 fun standard_term_uncheck ctxt =
   map (contract_abbrevs ctxt);
 
-fun add what f = Context.add_setup
-  (Context.theory_map (what (fn xs => fn ctxt => (f ctxt xs, ctxt))));
+fun add eq what f = Context.add_setup
+  (Context.theory_map (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 (Syntax.add_typ_check 0 "standard") standard_typ_check;
-val _ = add (Syntax.add_term_check 0 "standard") standard_term_check;
-val _ = add (Syntax.add_term_check 100 "fixate") prepare_patterns;
+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 (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
+val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
 
 end;
 

--- a/src/Pure/Syntax/syntax.ML	Tue Oct 16 19:45:56 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Oct 16 19:45:57 2007 +0200
@@ -105,16 +105,16 @@
     unparse_term: Proof.context -> term -> Pretty.T} -> unit
   val print_checks: Proof.context -> unit
   val add_typ_check: int -> string ->
-    (typ list -> Proof.context -> typ list * Proof.context) ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val add_term_check: int -> string ->
-    (term list -> Proof.context -> term list * Proof.context) ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
   val add_typ_uncheck: int -> string ->
-    (typ list -> Proof.context -> typ list * Proof.context) ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val add_term_uncheck: int -> string ->
-    (term list -> Proof.context -> term list * Proof.context) ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
@@ -684,7 +684,7 @@
 local
 
 type key = int * bool;
-type 'a check = 'a list -> Proof.context -> 'a list * Proof.context;
+type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
 
 structure Checks = GenericDataFun
 (
@@ -701,19 +701,16 @@
 fun gen_add which (key: key) name f =
   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
 
-fun gen_check which uncheck eq ctxt0 xs0 =
+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)
-      |> not uncheck ? map (apsnd rev);
-
-    fun check_fixpoint fs (xs, ctxt) =
-      let val (xs', ctxt') = fold uncurry fs (xs, ctxt) in
-        if eq_list eq (xs, xs') then (xs, ctxt)
-        else check_fixpoint fs (xs', ctxt')
-      end;
-  in #1 (fold (check_fixpoint o snd) funs (xs0, ctxt0)) end;
+      |> 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
@@ -748,8 +745,8 @@
 fun add_typ_uncheck stage = gen_add apfst (stage, true);
 fun add_term_uncheck stage = gen_add apsnd (stage, true);
 
-val check_typs = gen_check fst false (op =);
-val check_terms = gen_check snd false (op aconv);
+val check_typs = gen_check fst false;
+val check_terms = gen_check snd false;
 fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt;
 
 val check_typ = singleton o check_typs;
@@ -757,8 +754,8 @@
 val check_prop = singleton o check_props;
 val check_sort = map_sort o check_typ;
 
-val uncheck_typs = gen_check fst true (op =);
-val uncheck_terms = gen_check snd true (op aconv);
+val uncheck_typs = gen_check fst true;
+val uncheck_terms = gen_check snd true;
 val uncheck_sort = map_sort o singleton o uncheck_typs;
 
 end;