--- a/src/Pure/Isar/args.ML Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Isar/args.ML Sun Mar 09 16:37:56 2014 +0100
@@ -208,11 +208,11 @@
(* type and constant names *)
fun type_name flags =
- Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
+ Scan.peek (named_typ o Proof_Context.read_type_name flags o Context.proof_of)
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
fun const flags =
- Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
+ Scan.peek (named_term o Proof_Context.read_const flags o Context.proof_of)
>> (fn Const (c, _) => c | Free (x, _) => x | _ => "");