--- a/QuotMain.thy	Sun Dec 06 01:43:46 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 02:41:35 2009 +0100
@@ -1051,8 +1051,10 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
+thm lambda_prs
+
 ML {*
-fun lambda_allex_prs_simple_conv ctxt ctrm =
+fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
     let
@@ -1074,10 +1076,10 @@
 *}
 
 ML {*
-val lambda_allex_prs_conv =
-  More_Conv.top_conv lambda_allex_prs_simple_conv
+val lambda_prs_conv =
+  More_Conv.top_conv lambda_prs_simple_conv
 
-fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
 (*