src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/HOL.thy	Wed Mar 04 22:05:01 2015 +0100
@@ -1223,7 +1223,7 @@
         let
           val n = case f of (Abs (x, _, _)) => x | _ => "x";
           val cx = Thm.cterm_of thy x;
-          val {T = xT, ...} = Thm.rep_cterm cx;
+          val xT = Thm.typ_of_cterm cx;
           val cf = Thm.cterm_of thy f;
           val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
           val (_ $ _ $ g) = Thm.prop_of fx_g;