# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258768403 -3600
# Node ID d741ccea80d32b0d4fcfcc7457a6d32b9148a1e0
# Parent  f46dc0ca08c3201d9001ae43efba75ea0268d429
flagged qenv-stuff as obsolete

diff -r f46dc0ca08c3 -r d741ccea80d3 quotient_info.ML
--- a/quotient_info.ML	Sat Nov 21 02:49:39 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 02:53:23 2009 +0100
@@ -12,6 +12,7 @@
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
+  (*FIXME: obsolete *)
   type qenv = (typ * typ) list
   val mk_qenv: Proof.context -> qenv
   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option