# 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) =