diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_tacs.ML
--- a/Attic/Quot/quotient_tacs.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_tacs.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_tacs.thy
+(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Tactics for solving goal arising from lifting
-    theorems to quotient types.
+Tactics for solving goal arising from lifting theorems to quotient
+types.
 *)
 
 signature QUOTIENT_TACS =
@@ -89,7 +89,7 @@
 fun get_match_inst thy pat trm =
 let
   val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ             (* raises BIND, if no unifier *)
+  val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *)  (* FIXME fragile *)
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv = Vartab.dest (Envir.type_env env)
 in