src/Pure/goal.ML
changeset 20290 3f886c176c9b
parent 20260 990dbc007ca6
child 21516 c2a116a2c4fd
     1.1 --- a/src/Pure/goal.ML	Wed Aug 02 22:26:41 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Wed Aug 02 22:26:44 2006 +0200
     1.3 @@ -21,10 +21,10 @@
     1.4    val compose_hhf_tac: thm -> int -> tactic
     1.5    val comp_hhf: thm -> thm -> thm
     1.6    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.7 -  val prove_multi: Context.proof -> string list -> term list -> term list ->
     1.8 -    ({prems: thm list, context: Context.proof} -> tactic) -> thm list
     1.9 -  val prove: Context.proof -> string list -> term list -> term ->
    1.10 -    ({prems: thm list, context: Context.proof} -> tactic) -> thm
    1.11 +  val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.12 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    1.13 +  val prove: Proof.context -> string list -> term list -> term ->
    1.14 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.15    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.16    val extract: int -> int -> thm -> thm Seq.seq
    1.17    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    1.18 @@ -39,7 +39,9 @@
    1.19    -------- (init)
    1.20    C ==> #C
    1.21  *)
    1.22 -fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI;
    1.23 +val init =
    1.24 +  let val A = #1 (Drule.dest_implies (Thm.cprop_of Drule.protectI))
    1.25 +  in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
    1.26  
    1.27  (*
    1.28     C
    1.29 @@ -132,7 +134,7 @@
    1.30        orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    1.31    in
    1.32      results
    1.33 -    |> (Seq.hd o Assumption.exports false ctxt' ctxt)
    1.34 +    |> map (Assumption.export false ctxt' ctxt)
    1.35      |> Variable.export ctxt' ctxt
    1.36      |> map Drule.zero_var_indexes
    1.37    end;