simplified Proof.end_block;
authorwenzelm
Wed Aug 02 22:26:59 2006 +0200 (2006-08-02 ago)
changeset 2030516c8f44b1852
parent 20304 500a3373c93c
child 20306 614b7e6c6276
simplified Proof.end_block;
src/Pure/Isar/isar_syn.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:58 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:59 2006 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4  val endP =
     1.5    OuterSyntax.command "}" "end explicit proof block"
     1.6      (K.tag_proof K.prf_close)
     1.7 -    (Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block));
     1.8 +    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
     1.9  
    1.10  val nextP =
    1.11    OuterSyntax.command "next" "enter next proof block"
     2.1 --- a/src/Pure/Tools/invoke.ML	Wed Aug 02 22:26:58 2006 +0200
     2.2 +++ b/src/Pure/Tools/invoke.ML	Wed Aug 02 22:26:59 2006 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4         (("", []), map (rpair [] o Element.mark_witness) prems')];
     2.5      fun after_qed results =
     2.6        Proof.end_block #>
     2.7 -      Seq.map (Proof.map_context (fn ctxt =>
     2.8 +      Proof.map_context (fn ctxt =>
     2.9          let
    2.10            val ([res_types, res_params, res_prems], ctxt'') =
    2.11              fold_burrow (apfst snd oo Variable.import false) results ctxt';
    2.12 @@ -82,7 +82,8 @@
    2.13            |> ProofContext.qualified_names
    2.14            |> (snd o ProofContext.note_thmss_i notes)
    2.15            |> ProofContext.restore_naming ctxt
    2.16 -        end) #> Proof.put_facts NONE);
    2.17 +        end) #>
    2.18 +      Proof.put_facts NONE #> Seq.single;
    2.19    in
    2.20      state'
    2.21      |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i