src/Pure/Isar/expression.ML
changeset 54878 710e8f36a917
parent 54877 0a9337337277
child 54879 a9397557da56
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:13 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:14 2013 +0100
     1.3 @@ -403,8 +403,8 @@
     1.4      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
     1.5  
     1.6      (* Retrieve parameter types *)
     1.7 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
     1.8 -      | _ => fn ps => ps) (Fixes fors :: elems') [];
     1.9 +    val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
    1.10 +      (Fixes fors :: elems');
    1.11      val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    1.12      val parms = xs ~~ Ts;  (* params from expression and elements *)
    1.13