# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257172765 -3600
# Node ID 9279f95e574a2a48abe4f1ef342f516def8027c2
# Parent  34fb63221536ce0a4e44af22efd0a2884550cc7f# Parent  59578f428bbe6b3f825af5c994f7044699cadf9e
merged

diff -r 59578f428bbe -r 9279f95e574a IntEx.thy
--- a/IntEx.thy	Mon Nov 02 15:38:03 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 15:39:25 2009 +0100
@@ -19,7 +19,6 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
-thm ZERO_def
 
 quotient_def (for my_int)
   ONE::"my_int"
diff -r 59578f428bbe -r 9279f95e574a QuotMain.thy
--- a/QuotMain.thy	Mon Nov 02 15:38:03 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 15:39:25 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 *}