src/Pure/Isar/expression.ML

     val ctxt4 = init_body ctxt3;
     val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
     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 *)
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';