# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259805234 -3600
# Node ID 3a4da8a6384024f66f8d6a61efd243797b70686d
# Parent  5214ec75add48d6912509cc413c00fe892fd55e0
further simplification

diff -r 5214ec75add4 -r 3a4da8a63840 QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 02:18:21 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 02:53:54 2009 +0100
@@ -1121,10 +1121,7 @@
 *}
 
 ML {*
-fun lambda_prs_tac quot ctxt = CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (lambda_prs_conv quot ctxt) then_conv
-          Conv.concl_conv ~1 (lambda_prs_conv quot ctxt))) ctxt) 
+fun lambda_prs_tac quot ctxt = CONVERSION (lambda_prs_conv quot ctxt)
 *}
 
 (*