diff -r da75568e7f12 -r bf6861ee3b90 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Dec 23 23:22:02 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 23:53:03 2009 +0100
@@ -145,7 +145,7 @@
        if s = s' 
        then 
          let
-           val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") 
+           val exc = LIFT_MATCH ("mk_resp_arg (no relation map function found for type " ^ s ^ ")") 
            val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc
            val args = map (mk_resp_arg ctxt) (tys ~~ tys')
          in
@@ -188,7 +188,7 @@
 
 (* produces a regularized version of rtrm       *)
 (*                                              *)
-(* - the result still contains dummyTs          *)
+(* - the result might contain dummyTs           *)
 (*                                              *)
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
@@ -228,7 +228,7 @@
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
-         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
+         val rel_ty = fastype_of rel
          val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') 
        in 
          if rel' aconv rel then rtrm else raise exc
@@ -258,7 +258,7 @@
              val qtrm_str = Syntax.string_of_term ctxt qtrm
              val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
              val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
-             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
+             val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1
            in 
              if Pattern.matches thy (rtrm', rtrm) 
              then rtrm else raise exc2