--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat Jan 14 21:16:15 2012 +0100
@@ -284,8 +284,8 @@
| hidden_variable (Free f) = not (member (op =) tf f)
| hidden_variable _ = false;
- fun mk_default' T = list_abs
- (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
+ fun mk_default' T =
+ fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
fun elim_varst (t $ u) = elim_varst t $ elim_varst u
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)