QuotMain.thy
changeset 261 34fb63221536
parent 259 22c199522bef
child 263 a159ba20979e
--- 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 *}