
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)
 *}
 
 (*




