src/HOL/BNF/Tools/bnf_util.ML
changeset 51787 1267c28c7bdd
parent 51767 bbcdd8519253
child 51790 22517d04d20b
     1.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 09:53:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 11:04:45 2013 +0200
     1.3 @@ -159,8 +159,11 @@
     1.4    val certifyT: Proof.context -> typ -> ctyp
     1.5    val certify: Proof.context -> term -> cterm
     1.6  
     1.7 +  val standard_binding: binding
     1.8 +  val smart_binding: binding
     1.9 +  val binding_eq: binding * binding -> bool
    1.10    val parse_binding_colon: Token.T list -> binding * Token.T list
    1.11 -  val parse_opt_binding_colon: Token.T list -> binding * Token.T list
    1.12 +  val parse_opt_binding_colon: binding -> Token.T list -> binding * Token.T list
    1.13  
    1.14    val typedef: binding * (string * sort) list * mixfix -> term ->
    1.15      (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
    1.16 @@ -302,8 +305,16 @@
    1.17  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    1.18  fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    1.19  
    1.20 +val binding_eq = (op =) o pairself Binding.dest
    1.21 +
    1.22 +(* The standard binding stands for a name generated following the canonical convention (e.g.
    1.23 +   "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
    1.24 +   depending on the context. *)
    1.25 +val standard_binding = @{binding _};
    1.26 +val smart_binding = Binding.conceal standard_binding;
    1.27 +
    1.28  val parse_binding_colon = Parse.binding --| @{keyword ":"};
    1.29 -val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    1.30 +val parse_opt_binding_colon = Scan.optional parse_binding_colon;
    1.31  
    1.32  (*TODO: is this really different from Typedef.add_typedef_global?*)
    1.33  fun typedef typ set opt_morphs tac lthy =