# HG changeset patch
# User wenzelm
# Date 1191146114 -7200
# Node ID 1372969969e0cd15948cadbce13c7a11dc0afd8f
# Parent  123e219b66c2c4e653548ae351f82117301dcd45
standard_term_check: include expand_abbrevs (back again);

diff -r 123e219b66c2 -r 1372969969e0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Sep 29 21:39:53 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 30 11:55:14 2007 +0200
@@ -606,17 +606,19 @@
   map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
   map (prepare_patternT ctxt);
 
+fun standard_term_check ctxt =
+  standard_infer_types ctxt #>
+  map (expand_abbrevs ctxt);
+  
 fun add_check add f = Context.add_setup
   (Context.theory_map (add (fn xs => fn ctxt => (f ctxt xs, ctxt))));
 
 in
 
-val _ = add_check (Syntax.add_term_check 0 "standard") standard_infer_types;
-val _ = add_check (Syntax.add_term_check 50 "abbrevs") (map o expand_abbrevs);
+val _ = add_check (Syntax.add_typ_check 0 "standard") standard_typ_check;
+val _ = add_check (Syntax.add_term_check 0 "standard") standard_term_check;
 val _ = add_check (Syntax.add_term_check 100 "fixate") prepare_patterns;
 
-val _ = add_check (Syntax.add_typ_check 0 "standard") standard_typ_check;
-
 end;