diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 13 20:21:40 2010 +0200
@@ -780,9 +780,11 @@
      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
 fun rep_type_for_quot_type thy (T as Type (s, _)) =
-  let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
-    instantiate_type thy qtyp T rtyp
-  end
+    let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
+      instantiate_type thy qtyp T rtyp
+    end
+  | rep_type_for_quot_type _ T =
+    raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
     let
       val {qtyp, equiv_rel, equiv_thm, ...} =
@@ -1083,7 +1085,7 @@
   | _ => t
 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, stds, ...}) Ts new_T old_T t =
   if old_T = new_T then
     t
   else
@@ -1960,7 +1962,7 @@
     |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
   end
 
-fun codatatype_bisim_axioms (hol_ctxt as {thy, ctxt, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
   let
     val xs = datatype_constrs hol_ctxt T
     val set_T = T --> bool_T