--- a/src/Pure/Isar/expression.ML Sun Dec 29 23:21:13 2013 +0100
+++ b/src/Pure/Isar/expression.ML Sun Dec 29 23:21:14 2013 +0100
@@ -403,8 +403,8 @@
val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
- | _ => fn ps => ps) (Fixes fors :: elems') [];
+ val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
+ (Fixes fors :: elems');
val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)