diff -r bf6861ee3b90 -r d6407afb913c Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_term.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -154,7 +154,7 @@
        else 
          let
            val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") 
-           val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc
+           val equiv_rel = #equiv_rel (quotdata_lookup thy s') handle NotFound => raise exc
            (* FIXME: check in this case that the rty and qty *)
            (* FIXME: correspond to each other *)