# HG changeset patch
# User wenzelm
# Date 1320847128 -3600
# Node ID 92f91f990165ed3323401751b2882f2221275b59
# Parent  711dac69111b0dfe4a5db1798d6c37d97fdb086c
tuned signature -- emphasize internal role of these operations;

diff -r 711dac69111b -r 92f91f990165 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 09 14:30:03 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 09 14:58:48 2011 +0100
@@ -51,10 +51,10 @@
     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
-  val term_uncheck: Proof.context -> term list -> term list
+  val apply_typ_check: Proof.context -> typ list -> typ list
+  val apply_term_check: Proof.context -> term list -> term list
+  val apply_typ_uncheck: Proof.context -> typ list -> typ list
+  val apply_term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -322,10 +322,10 @@
 
 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 apply_typ_check = check fst false;
+val apply_term_check = check snd false;
+val apply_typ_uncheck = check fst true;
+val apply_term_uncheck = check snd true;
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
diff -r 711dac69111b -r 92f91f990165 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 14:30:03 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 14:58:48 2011 +0100
@@ -714,12 +714,16 @@
 
 (** check/uncheck **)
 
-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_typs ctxt =
+  Syntax.apply_typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt);
+
+fun check_terms ctxt =
+  Syntax.apply_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;
-val uncheck_terms = Syntax.term_uncheck;
+val uncheck_typs = Syntax.apply_typ_uncheck;
+val uncheck_terms = Syntax.apply_term_uncheck;