# HG changeset patch # User blanchet # Date 1384821014 -3600 # Node ID 0a99cd1db5d6c5d34fc19d86574cd01c3cdae071 # Parent d8d276c922f25904dc2123fd4454bb2853ce0625 tuning diff -r d8d276c922f2 -r 0a99cd1db5d6 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue Nov 19 01:30:14 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Nov 19 01:30:14 2013 +0100 @@ -1354,7 +1354,7 @@ val cTs = map (SOME o certifyT lthy o TFree) induct_params; val weak_ctor_induct_thms = - let fun insts i = (replicate (i - 1) TrueI) @ (@{thm asm_rl} :: replicate (n - i) TrueI); + let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI); in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end; val (ctor_induct2_thm, induct2_params) =