src/Pure/Isar/proof_context.ML
changeset 30211 556d1810cdad
parent 30190 479806475f3c
child 30218 cdd82ba2b4fd
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 14:07:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 14:07:43 2009 +0100
     1.3 @@ -103,12 +103,10 @@
     1.4    val sticky_prefix: string -> Proof.context -> Proof.context
     1.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
     1.6    val reset_naming: Proof.context -> Proof.context
     1.7 -  val note_thmss: string ->
     1.8 -    ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
     1.9 -      Proof.context -> (string * thm list) list * Proof.context
    1.10 -  val note_thmss_i: string ->
    1.11 -    ((binding * attribute list) * (thm list * attribute list) list) list ->
    1.12 -      Proof.context -> (string * thm list) list * Proof.context
    1.13 +  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
    1.14 +    Proof.context -> (string * thm list) list * Proof.context
    1.15 +  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
    1.16 +    Proof.context -> (string * thm list) list * Proof.context
    1.17    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    1.18    val read_vars: (binding * string option * mixfix) list -> Proof.context ->
    1.19      (binding * typ option * mixfix) list * Proof.context
    1.20 @@ -121,10 +119,10 @@
    1.21    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
    1.22    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
    1.23    val add_assms: Assumption.export ->
    1.24 -    ((binding * attribute list) * (string * string list) list) list ->
    1.25 +    (Thm.binding * (string * string list) list) list ->
    1.26      Proof.context -> (string * thm list) list * Proof.context
    1.27    val add_assms_i: Assumption.export ->
    1.28 -    ((binding * attribute list) * (term * term list) list) list ->
    1.29 +    (Thm.binding * (term * term list) list) list ->
    1.30      Proof.context -> (string * thm list) list * Proof.context
    1.31    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
    1.32    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context