changeset 36936 | c52d1c130898 |
parent 36850 | 0ea667bb5be7 |
child 36945 | 9bec62c10714 |
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 15:31:33 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 17:59:06 2010 +0200 @@ -490,7 +490,7 @@ end | _ => Conv.all_conv ctrm -fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt +fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)