--- a/src/Pure/Syntax/syntax_phases.ML Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Jul 13 20:36:18 2011 +0200
@@ -709,8 +709,8 @@
(** check/uncheck **)
-val check_typs = Syntax.typ_check;
-val check_terms = Syntax.term_check;
+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);
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
val uncheck_typs = Syntax.typ_uncheck;