# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263294873 -3600
# Node ID 9a0a0b92e8fec5d0098cf85b8cc4c620de88647e
# Parent  9531fafc0daa11b7efc3541bfc6343f765f4c9e7
handle all is no longer necessary in lambda_prs.

diff -r 9531fafc0daa -r 9a0a0b92e8fe Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 12 12:04:47 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 12 12:14:33 2010 +0100
@@ -459,36 +459,34 @@
   (f, Abs ("x", T, mk_abs u 0 g))
 end
 
-(* Simplifies a redex using the 'lambda_prs' theorem.        *)
-(* First instantiates the types and known subterms.          *)
-(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
-(* Finally instantiates the function f using make_inst       *)
-(* If Rep2 is an identity then the pattern is simpler and    *)
-(* make_inst_id is used                                      *)
+(* Simplifies a redex using the 'lambda_prs' theorem.
+   First instantiates the types and known subterms.
+   Then solves the quotient assumptions to get Rep2 and Abs1
+   Finally instantiates the function f using make_inst
+   If Rep2 is an identity then the pattern is simpler and
+   make_inst_id is used *)
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-   (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
-     (let
-       val thy = ProofContext.theory_of ctxt
-       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
-       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
-       val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
-       val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
-       val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
-       val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
-       val (insp, inst) = 
-              if ty_c = ty_d 
-              then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
-              else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
-       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-     in
-       Conv.rewr_conv ti ctrm
-     end
-     handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *)
+    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+      let
+        val thy = ProofContext.theory_of ctxt
+        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+        val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
+        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+        val (insp, inst) =
+          if ty_c = ty_d
+          then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
+          else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+      in
+        Conv.rewr_conv ti ctrm
+      end
   | _ => Conv.all_conv ctrm
 
-
 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)