src/HOL/HOL.thy
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/HOL/HOL.thy	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -1223,7 +1223,7 @@
     1.4          let
     1.5            val n = case f of (Abs (x, _, _)) => x | _ => "x";
     1.6            val cx = Thm.cterm_of thy x;
     1.7 -          val {T = xT, ...} = Thm.rep_cterm cx;
     1.8 +          val xT = Thm.typ_of_cterm cx;
     1.9            val cf = Thm.cterm_of thy f;
    1.10            val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    1.11            val (_ $ _ $ g) = Thm.prop_of fx_g;