diff -r a6a4c88e1c9a -r 09a64cb04851 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Jan 14 15:36:29 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 14 16:41:17 2010 +0100
@@ -4,6 +4,8 @@
 
   datatype flag = absF | repF
 
+  val absrep_const_chk: flag -> Proof.context -> string -> term
+
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
@@ -126,6 +128,9 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
+fun absrep_const_chk flag ctxt qty_str =
+  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+
 fun absrep_match_err ctxt ty_pat ty =
 let
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat