diff -r 8ebdef196fd5 -r a031bcaf6719 quotient_def.ML
--- a/quotient_def.ML	Thu Nov 05 09:38:34 2009 +0100
+++ b/quotient_def.ML	Thu Nov 05 09:55:21 2009 +0100
@@ -128,7 +128,7 @@
 
 fun sanity_chk lthy qenv =
 let
-  val qenv' = Quotient_Info.mk_qenv lthy
+  val global_qenv = Quotient_Info.mk_qenv lthy
   val thy = ProofContext.theory_of lthy
 
   fun is_inst thy (qty, rty) (qty', rty') =
@@ -141,7 +141,8 @@
   else false
 
   fun chk_inst (qty, rty) = 
-    if exists (is_inst thy (qty, rty)) qenv' then true
+    if exists (is_inst thy (qty, rty)) global_qenv 
+    then true
     else error_msg lthy (qty, rty)
 in
   forall chk_inst qenv