--- a/Quot/quotient_tacs.ML	Mon Jan 11 15:13:09 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Jan 11 15:58:38 2010 +0100
@@ -93,26 +93,26 @@
   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 
-(* calculates the instantiations for the lemmas *)
-(* ball_reg_eqv_range and bex_reg_eqv_range     *)
+(* Calculates the instantiations for the lemmas:
+      ball_reg_eqv_range and bex_reg_eqv_range
+   Since the left-hand-side contains a non-pattern '?P (f ?x)'
+   we rely on unification/instantiation to check whether the
+   theorem applies and return NONE if it doesn't. *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
 let
   fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
   val thy = ProofContext.theory_of ctxt
   val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
   val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
-  val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm (* raises TYPE *)
-  val inst2 = get_match_inst thy (get_lhs thm') redex
-  val thm'' =  Drule.instantiate inst2 thm'                      (* raises THM *)
 in
-  SOME thm''
+  (case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of
+    NONE => NONE
+  | SOME thm' =>
+      (case try (get_match_inst thy (get_lhs thm')) redex of
+        NONE => NONE
+      | SOME inst2 => try (Drule.instantiate inst2) thm')
+  )
 end
-handle _ => NONE      
-(* FIXME/TODO: !!!CLEVER CODE!!!                                       *)
-(* FIXME/TODO: What are the places where the exceptions are raised,    *)
-(* FIXME/TODO: and which exception is it?                              *)
-(* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *)
-(* FIXME/TODO: when NONE should be returned?                           *)
 
 fun ball_bex_range_simproc ss redex =
 let
@@ -222,7 +222,6 @@
 fun dest_comb (f $ a) = (f, a) 
 fun dest_bcomb ((_ $ l) $ r) = (l, r) 
 
-(* TODO: Can this be done easier? *)
 fun unlam t =
   case t of
     (Abs a) => snd (Term.dest_abs a)
@@ -265,17 +264,14 @@
 let
   val ty = domain_type (fastype_of R);
   val thy = ProofContext.theory_of ctxt
-  val thm = Drule.instantiate' 
-               [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
 in
-  rtac thm THEN' quotient_tac ctxt
+  case try (Drule.instantiate' [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)])
+    @{thm equals_rsp} of
+    NONE => K no_tac
+  | SOME thm => rtac thm THEN' quotient_tac ctxt
 end
-(* TODO: Are they raised by instantiate'?              *)
 (* TODO: Again, can one specify more concretely        *)
 (* TODO: in terms of R when no_tac should be returned? *)
-handle THM _  => K no_tac  
-     | TYPE _ => K no_tac    
-     | TERM _ => K no_tac
 
 fun rep_abs_rsp_tac ctxt = 
   SUBGOAL (fn (goal, i) =>