src/Pure/goal.ML
changeset 26713 1c6181def1d0
parent 26628 63306cb94313
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/goal.ML	Thu Apr 17 22:22:23 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Apr 17 22:22:25 2008 +0200
     1.3 @@ -25,7 +25,8 @@
     1.4      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
     1.5    val prove: Proof.context -> string list -> term list -> term ->
     1.6      ({prems: thm list, context: Proof.context} -> tactic) -> thm
     1.7 -  val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.8 +  val prove_global: theory -> string list -> term list -> term ->
     1.9 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.10    val extract: int -> int -> thm -> thm Seq.seq
    1.11    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    1.12    val conjunction_tac: int -> tactic
    1.13 @@ -120,7 +121,8 @@
    1.14      val (prems, ctxt') = ctxt
    1.15        |> Variable.add_fixes_direct xs
    1.16        |> fold Variable.declare_internal (asms @ props)
    1.17 -      |> Assumption.add_assumes casms;
    1.18 +      |> Assumption.add_assumes casms
    1.19 +      ||> Variable.set_body true;
    1.20  
    1.21      val goal = init (Conjunction.mk_conjunction_balanced cprops);
    1.22      val res =
    1.23 @@ -144,7 +146,7 @@
    1.24  fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    1.25  
    1.26  fun prove_global thy xs asms prop tac =
    1.27 -  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
    1.28 +  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    1.29  
    1.30  
    1.31