changeset 52844 | 66fa0f602cc4 |
parent 52813 | 963297a24206 |
child 52923 | ec63c82551ae |
--- a/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 02 21:52:45 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 02 22:36:31 2013 +0200 @@ -1107,7 +1107,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl))) - (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono)) + (K (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))) |> Thm.close_derivation end;