diff -r 97f6e5c61f03 -r cdc6ae1a4ed2 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 23:35:02 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 00:07:23 2009 +0100
@@ -1083,7 +1083,7 @@
 ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-   ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+   ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
      let
        val thy = ProofContext.theory_of ctxt
        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -1096,9 +1096,14 @@
        val tl = Thm.lhs_of ts
        val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-        (*val _ = tracing "lambda_prs"
-          val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
-          val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+       val _ = if not (s = @{const_name "id"}) then
+                  (tracing "lambda_prs";
+                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+                   tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+                   tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+                   tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+               else ()
      in
        Conv.rewr_conv ti ctrm
      end