src/HOL/Tools/Quotient/quotient_def.ML

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -51,7 +51,7 @@
 
     fun sanity_test NONE _ = true
       | sanity_test (SOME bind) str =
-          if Name.of_binding bind = str then true
+          if Variable.name bind = str then true
           else error_msg bind str
 
     val _ = sanity_test optbind lhs_str