# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1258030640 -3600
# Node ID 7af81ea081d6d436945f468d9881b09b7f7b0633
# Parent  3b3c5feb6b73acb79003b14c94db92a93cfb4f49# Parent  23aa8596dcd3fe84c5f8790318b9e67f5b9c5fbc
merge of the merge?

diff -r 3b3c5feb6b73 -r 7af81ea081d6 quotient.ML
--- a/quotient.ML	Thu Nov 12 13:56:07 2009 +0100
+++ b/quotient.ML	Thu Nov 12 13:57:20 2009 +0100
@@ -147,8 +147,9 @@
 
   (* storing the quot-info *)
   val qty_str = fst (dest_Type abs_ty)		  
-  val lthy3 = quotdata_update qty_str 
-                                (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  (* FIXME: varifyT should not be used *)
+  (* the type name maybe should be calculated via qty_name and Sign.intern_type *} 
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))