# HG changeset patch # User wenzelm # Date 1236204332 -3600 # Node ID 970bf4f594c94ede73a5f9930c7e7c8c07e7f83e # Parent 2ec2df1a1665c195a86516eeb6477fdb5d5c0f20 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking; diff -r 2ec2df1a1665 -r 970bf4f594c9 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Wed Mar 04 19:22:32 2009 +0000 +++ b/src/Pure/ML/ml_thms.ML Wed Mar 04 23:05:32 2009 +0100 @@ -48,25 +48,30 @@ (* ad-hoc goals *) +val and_ = Args.$$$ "and"; val by = Args.$$$ "by"; -val goal = Scan.unless (Scan.lift by) Args.prop; +val goal = Scan.unless (by || and_) Args.name; val _ = ML_Context.add_antiq "lemma" - (fn pos => Args.context -- Args.mode "open" -- Scan.repeat1 goal -- - Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >> - (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} => + (fn pos => Args.context -- Args.mode "open" -- + Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) -- + (by |-- Method.parse -- Scan.option Method.parse)) >> + (fn ((ctxt, is_open), (raw_propss, methods)) => fn {struct_name, background} => let + val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; val i = serial (); val prep_result = Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation; - fun after_qed [res] goal_ctxt = - put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt; + fun after_qed res goal_ctxt = + put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt; val ctxt' = ctxt - |> Proof.theorem_i NONE after_qed [map (rpair []) props] + |> Proof.theorem_i NONE after_qed propss |> 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); + val ml = + (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, + struct_name ^ "." ^ a); in (K ml, background') end)); end;