# HG changeset patch
# User wenzelm
# Date 1369135367 -7200
# Node ID e58762f346399301beebdd60626e95014ae0b45c
# Parent  6225d5b308f903d7f6a52e028e14298076d8c712
proper context;

diff -r 6225d5b308f9 -r e58762f34639 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 21 12:03:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 21 13:22:47 2013 +0200
@@ -1731,12 +1731,13 @@
               ctors (0 upto n - 1) witss
           end;
 
-        fun wit_tac ctxt _ = mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
+        fun wit_tac {context = ctxt, prems = _} =
+          mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
           fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
               fn T => fn wits => fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac lthy) (SOME deads)
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
               map_b rel_b set_bs
               (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
               lthy