# HG changeset patch
# User blanchet
# Date 1366813283 -7200
# Node ID 0051318acc9dba243625822005fc3a92ef58145e
# Parent  219a3063ed29281213098540ff4e5fc5365b2980
apply arguments to f and g in "case_cong"

diff -r 219a3063ed29 -r 0051318acc9d src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 15:42:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 16:21:23 2013 +0200
@@ -570,12 +570,12 @@
 
         val (case_cong_thm, weak_case_cong_thm) =
           let
-            fun mk_prem xctr xs f g =
+            fun mk_prem xctr xs xf xg =
               fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
-                mk_Trueprop_eq (f, g)));
+                mk_Trueprop_eq (xf, xg)));
 
             val goal =
-              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss fs gs,
+              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
                  mk_Trueprop_eq (eta_ufcase, eta_vgcase));
             val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
           in