# HG changeset patch
# User wenzelm
# Date 1215689854 -7200
# Node ID 44081396d73534499e0b996ee4b2f81b3298b240
# Parent  fb07f3b328630d37840fd5d7a92fd4b0a3be3e9a
@{lemma}: allow terminal method, close derivation unless (open) mode is given;

diff -r fb07f3b32863 -r 44081396d735 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Jul 10 13:37:33 2008 +0200
+++ b/src/Pure/ML/ml_thms.ML	Thu Jul 10 13:37:34 2008 +0200
@@ -53,15 +53,17 @@
 val goal = Scan.unless by Args.prop;
 
 val _ = ML_Context.add_antiq "lemma"
-  ((Args.context -- Scan.repeat1 goal -- (by |-- Scan.lift Method.parse_args)) >>
-    (fn ((ctxt, props), method_text) => fn {struct_name, background} =>
+  ((Args.context -- Args.mode "open" -- Scan.repeat1 goal --
+      (by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >>
+    (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
       let
         val i = serial ();
+        val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
         fun after_qed [res] goal_ctxt =
-          put_thms (i, map Goal.norm_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt;
+          put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt;
         val ctxt' = ctxt
           |> Proof.theorem_i NONE after_qed [map (rpair []) props]
-          |> Proof.global_terminal_proof (method_text, NONE);
+          |> Proof.global_terminal_proof methods;
         val (a, background') = background
           |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
         val ml = (thm_bind (if length props = 1 then "thm" else "thms") a i, struct_name ^ "." ^ a);