1.1 --- a/src/Pure/Isar/proof.ML	Sun May 07 00:21:13 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun May 07 00:22:05 2006 +0200
     1.3 @@ -47,23 +47,15 @@
     1.4    val fix: (string * string option) list -> state -> state
     1.5    val fix_i: (string * typ option) list -> state -> state
     1.6    val assm: ProofContext.export ->
     1.7 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     1.8 -    state -> state
     1.9 +    ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    1.10    val assm_i: ProofContext.export ->
    1.11 -    ((string * attribute list) * (term * (term list * term list)) list) list
    1.12 -    -> state -> state
    1.13 -  val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.14 -    state -> state
    1.15 -  val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
    1.16 -    -> state -> state
    1.17 -  val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
    1.18 -    -> state -> state
    1.19 -  val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
    1.20 -    -> state -> state
    1.21 -  val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
    1.22 -    state -> state
    1.23 -  val def_i: ((string * attribute list) * (string * (term * term list))) list ->
    1.24 -    state -> state
    1.25 +    ((string * attribute list) * (term * term list) list) list -> state -> state
    1.26 +  val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    1.27 +  val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
    1.28 +  val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    1.29 +  val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
    1.30 +  val def: ((string * Attrib.src list) * (string * (string * string list))) list -> state -> state
    1.31 +  val def_i: ((string * attribute list) * (string * (term * term list))) list -> state -> state
    1.32    val chain: state -> state
    1.33    val chain_facts: thm list -> state -> state
    1.34    val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
    1.35 @@ -114,25 +106,19 @@
    1.36    val global_done_proof: state -> context * theory
    1.37    val global_skip_proof: bool -> state -> context * theory
    1.38    val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    1.39 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.40 -    bool -> state -> state
    1.41 +    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
    1.42    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    1.43 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
    1.44 -    bool -> state -> state
    1.45 +    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
    1.46    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    1.47 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.48 -    bool -> state -> state
    1.49 +    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
    1.50    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    1.51 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
    1.52 -    bool -> state -> state
    1.53 +    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
    1.54    val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
    1.55      string option -> string * Attrib.src list ->
    1.56 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.57 -    context -> state
    1.58 +    ((string * Attrib.src list) * (string * string list) list) list -> context -> state
    1.59    val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
    1.60      string option -> string * attribute list ->
    1.61 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
    1.62 -    context -> state
    1.63 +    ((string * attribute list) * (term * term list) list) list -> context -> state
    1.64  end;
    1.65  
    1.66  structure Proof: PROOF =
    1.67 @@ -580,7 +566,7 @@
    1.68    in
    1.69      state'
    1.70      |> fix (map (rpair NONE) xs)
    1.71 -    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
    1.72 +    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs)
    1.73    end;
    1.74  
    1.75  in
    1.76 @@ -681,7 +667,7 @@
    1.77      val atts = map (prep_att (theory_of state)) raw_atts;
    1.78      val (asms, state') = state |> map_context_result (fn ctxt =>
    1.79        ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
    1.80 -    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
    1.81 +    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
    1.82    in
    1.83      state'
    1.84      |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)