goal statements: accomodate before_qed argument;

--- a/src/Pure/Isar/isar_thy.ML	Sat Oct 15 00:08:03 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Oct 15 00:08:04 2005 +0200
@@ -102,10 +102,10 @@
 local
 
 fun local_goal opt_chain goal stmt int =
-  opt_chain #> goal (K (K Seq.single)) stmt int;
+  opt_chain #> goal NONE (K (K Seq.single)) stmt int;
 
 fun global_goal goal kind a propp thy =
-  goal kind (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
+  goal kind NONE (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
 
 in
 

--- a/src/Pure/axclass.ML	Sat Oct 15 00:08:03 2005 +0200
+++ b/src/Pure/axclass.ML	Sat Oct 15 00:08:04 2005 +0200
@@ -315,7 +315,7 @@
 
 fun gen_instance mk_prop add_thms inst thy = thy
   |> ProofContext.init
-  |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", [])
+  |> Proof.theorem_i Drule.internalK NONE (K (fold add_thms)) NONE ("", [])
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
 
 in