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