src/HOL/HOL.thy
changeset 46497 89ccf66aa73d
parent 46190 a42c5f23109f
child 46950 d0181abdbdac
--- a/src/HOL/HOL.thy	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 15 23:19:30 2012 +0100
@@ -1271,7 +1271,7 @@
           val cx = cterm_of thy x;
           val {T = xT, ...} = rep_cterm cx;
           val cf = cterm_of thy f;
-          val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
+          val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
           val (_ $ _ $ g) = prop_of fx_g;
           val g' = abstract_over (x,g);
         in (if (g aconv g')