# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264667300 -3600
# Node ID 07504636d14c54e7922b6312c390b14fd177ed5b
# Parent  ab45b11803ca0b8899843109ea48ea27de843a97# Parent  d44fda0cf39329211f76a81b8b316b3418ab7aba
merged

diff -r ab45b11803ca -r 07504636d14c Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Thu Jan 28 09:28:06 2010 +0100
+++ b/Quot/Nominal/Test.thy	Thu Jan 28 09:28:20 2010 +0100
@@ -117,11 +117,11 @@
     if is_atom tyS then HOLogic.mk_set ty [t] else
     if (Long_Name.base_name tyS) mem dt_names then 
       Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t else
-    @{term "{}"}
+    HOLogic.mk_set @{typ name} []
   val fv_eq = 
-    if null vars then HOLogic.mk_set @{typ atom} []
+    if null vars then HOLogic.mk_set @{typ name} []
     else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
-  val fv_eq_str = Syntax.string_of_term lthy fv_eq
+  val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq)
 in
   prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str
 end
diff -r ab45b11803ca -r 07504636d14c Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Jan 28 09:28:06 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 28 09:28:20 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