# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261464136 -3600
# Node ID a95f6bb081cf6fce81149a56e74919ad6a6d689f
# Parent  b2231990b059e24256dfdc62c0fa7ccfff287f6f
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst

diff -r b2231990b059 -r a95f6bb081cf Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Dec 22 07:28:09 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 07:42:16 2009 +0100
@@ -56,23 +56,16 @@
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-fun solve_equiv_assm ctxt thm =
-  case Seq.pull (equiv_tac ctxt 1 thm) of
-    SOME (t, _) => t
-  | _ => error "solve_equiv_assm failed."
-
-
-
 fun prep_trm thy (x, (T, t)) =
   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
 fun prep_ty thy (x, (S, ty)) =
   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
 
-fun matching_prs thy pat trm =
+fun get_match_inst thy pat trm =
 let
   val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ
+  val SOME (env, _) = Seq.pull univ                              (* raises BIND, if no unifier *)
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv = Vartab.dest (Envir.type_env env)
 in
@@ -87,9 +80,9 @@
   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
-  val inst2 = matching_prs thy (get_lhs thm') redex
-  val thm'' =  Drule.instantiate inst2 thm'
+  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''
 end
@@ -105,7 +98,7 @@
 let
   val ctxt = Simplifier.the_context ss
 in 
- case redex of
+  case redex of
     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
         calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
@@ -153,12 +146,13 @@
 fun regularize_tac ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
-  val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
-  val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+  val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
+  val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
+  val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
-                       addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
+                       addsimprocs [simproc] 
+                       addSolver equiv_solver addSolver quotient_solver
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
 in
   simp_tac simpset THEN'