# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260063695 -3600
# Node ID 9c6991411e1fa3421240d657b0fd73ae664839ad
# Parent  6a031829319a1d612ef0716c91b3cd9ab6ce433b
renamed lambda_allex_prs

diff -r 6a031829319a -r 9c6991411e1f QuotMain.thy
--- 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)
 *}
 
 (*