--- a/Quot/quotient_tacs.ML	Sat Dec 19 22:04:34 2009 +0100
+++ b/Quot/quotient_tacs.ML	Sat Dec 19 22:09:57 2009 +0100
@@ -564,6 +564,7 @@
   error msg
 end
 
+open Quotient_Term;
  
 fun procedure_inst ctxt rtrm qtrm =
 let

--- a/Quot/quotient_term.ML	Sat Dec 19 22:04:34 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 19 22:09:57 2009 +0100
@@ -46,26 +46,27 @@
     case (rty, qty) of
       (Type (s, tys), Type (s', tys')) =>
        if s = s' 
-       then let
-              val map_info = maps_lookup thy s
-                             handle NotFound => 
-                               raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
-              val args = map (mk_resp_arg lthy) (tys ~~ tys')
-            in
-              list_comb (Const (#relfun map_info, dummyT), args) 
-            end  
-       else let  
-              val SOME qinfo = quotdata_lookup_thy thy s'
-              (* FIXME: check in this case that the rty and qty *)
-              (* FIXME: correspond to each other *)
-              val (s, _) = dest_Const (#rel qinfo)
-              (* FIXME: the relation should only be the string        *)
-              (* FIXME: and the type needs to be calculated as below; *)
-              (* FIXME: maybe one should actually have a term         *)
-              (* FIXME: and one needs to force it to have this type   *)
-            in
-              Const (s, rty --> rty --> @{typ bool})
-            end
+       then 
+         let
+           val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
+           val map_info = maps_lookup thy s handle NotFound => raise exc
+           val args = map (mk_resp_arg lthy) (tys ~~ tys')
+         in
+           list_comb (Const (#relfun map_info, dummyT), args) 
+         end  
+       else 
+         let  
+           val SOME qinfo = quotdata_lookup_thy thy s'
+           (* FIXME: check in this case that the rty and qty *)
+           (* FIXME: correspond to each other *)
+           val (s, _) = dest_Const (#rel qinfo)
+           (* FIXME: the relation should only be the string        *)
+           (* FIXME: and the type needs to be calculated as below; *)
+           (* FIXME: maybe one should actually have a term         *)
+           (* FIXME: and one needs to force it to have this type   *)
+         in
+           Const (s, rty --> rty --> @{typ bool})
+         end
       | _ => HOLogic.eq_const dummyT 
              (* FIXME: check that the types correspond to each other? *)
 end
@@ -270,6 +271,5 @@
 
 end; (* structure *)
 
-open Quotient_Term;