src/Pure/Isar/args.ML
changeset 55954 a29aefc88c8d
parent 55951 c07d184aebe9
child 55955 e8f1bf005661
     1.1 --- a/src/Pure/Isar/args.ML	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Thu Mar 06 13:44:01 2014 +0100
     1.3 @@ -57,8 +57,7 @@
     1.4    val term_abbrev: term context_parser
     1.5    val prop: term context_parser
     1.6    val type_name: {proper: bool, strict: bool} -> string context_parser
     1.7 -  val const: bool -> string context_parser
     1.8 -  val const_proper: bool -> string context_parser
     1.9 +  val const: {proper: bool, strict: bool} -> string context_parser
    1.10    val goal_spec: ((int -> tactic) -> tactic) context_parser
    1.11    val parse: Token.T list parser
    1.12    val parse1: (string -> bool) -> Token.T list parser
    1.13 @@ -212,14 +211,10 @@
    1.14    Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
    1.15    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    1.16  
    1.17 -fun const strict =
    1.18 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
    1.19 +fun const flags =
    1.20 +  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags dummyT))
    1.21    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    1.22  
    1.23 -fun const_proper strict =
    1.24 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
    1.25 -  >> (fn Const (c, _) => c | _ => "");
    1.26 -
    1.27  
    1.28  (* improper method arguments *)
    1.29