src/HOL/BNF/Tools/bnf_util.ML
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 51757 7babcb61aa5c
     1.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 18:58:20 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 21:22:35 2012 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    val parse_binding_colon: Token.T list -> binding * Token.T list
     1.5    val parse_opt_binding_colon: Token.T list -> binding * Token.T list
     1.6  
     1.7 -  val typedef: binding option -> binding * (string * sort) list * mixfix -> term ->
     1.8 +  val typedef: binding * (string * sort) list * mixfix -> term ->
     1.9      (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
    1.10  
    1.11    val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    1.12 @@ -280,11 +280,11 @@
    1.13  val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    1.14  
    1.15  (*TODO: is this really different from Typedef.add_typedef_global?*)
    1.16 -fun typedef opt_name typ set opt_morphs tac lthy =
    1.17 +fun typedef typ set opt_morphs tac lthy =
    1.18    let
    1.19      val ((name, info), (lthy, lthy_old)) =
    1.20        lthy
    1.21 -      |> Typedef.add_typedef opt_name typ set opt_morphs tac
    1.22 +      |> Typedef.add_typedef typ set opt_morphs tac
    1.23        ||> `Local_Theory.restore;
    1.24      val phi = Proof_Context.export_morphism lthy_old lthy;
    1.25    in