--- 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;