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