# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264662819 -3600
# Node ID d44fda0cf39329211f76a81b8b316b3418ab7aba
# Parent  b582f7decd9a14eff6e5d9ae9203b40e99c5b3b6
Recommited the changes for nitpick

diff -r b582f7decd9a -r d44fda0cf393 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 18:26:01 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 28 08:13:39 2010 +0100
@@ -14,6 +14,9 @@
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
+  (* Allows Nitpick to represent quotient types as single elements from raw type *)
+  val absrep_const_chk: flag -> Proof.context -> string -> term
+
   val equiv_relation: Proof.context -> typ * typ -> term
   val equiv_relation_chk: Proof.context -> typ * typ -> term
 
@@ -133,6 +136,10 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
+(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+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