src/Pure/Isar/obtain.ML
changeset 29581 b3b33e0298eb
parent 29383 223f18cfbb32
child 30211 556d1810cdad
child 30240 5b25fee0362c
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -39,16 +39,16 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val thatN: string
     1.7 -  val obtain: string -> (Binding.T * string option * mixfix) list ->
     1.8 +  val obtain: string -> (binding * string option * mixfix) list ->
     1.9      (Attrib.binding * (string * string list) list) list ->
    1.10      bool -> Proof.state -> Proof.state
    1.11 -  val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
    1.12 -    ((Binding.T * attribute list) * (term * term list) list) list ->
    1.13 +  val obtain_i: string -> (binding * typ option * mixfix) list ->
    1.14 +    ((binding * attribute list) * (term * term list) list) list ->
    1.15      bool -> Proof.state -> Proof.state
    1.16    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
    1.17      (cterm list * thm list) * Proof.context
    1.18 -  val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.19 -  val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.20 +  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.21 +  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.22  end;
    1.23  
    1.24  structure Obtain: OBTAIN =