--- a/IntEx.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 15:38:49 2009 +0100
@@ -19,7 +19,6 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
-thm ZERO_def
 
 quotient_def (for my_int)
   ONE::"my_int"

--- a/QuotMain.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 15:38:49 2009 +0100
@@ -3,6 +3,8 @@
 uses ("quotient.ML")
 begin
 
+ML {* Attrib.empty_binding *}
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -300,11 +302,11 @@
 fun build_qenv lthy qtys = 
 let
   val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
+  val thy = ProofContext.theory_of lthy
   
   fun find_assoc ((qty', rty')::rest) qty =
         let 
-          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
+          val inst = Sign.typ_match thy (qty', qty) Vartab.empty
         in
            (Envir.norm_type inst qty, Envir.norm_type inst rty')
         end
@@ -343,7 +345,6 @@
   OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
 *}
 
-(* ML {* show_all_types := true *} *)
 
 section {* ATOMIZE *}