clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);

--- a/src/Pure/Isar/proof.ML	Fri Oct 02 20:51:32 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Oct 02 21:39:06 2009 +0200
@@ -431,9 +431,7 @@
 
 val refine = apply_text true;
 val refine_end = apply_text false;
-
-fun refine_insert [] = I
-  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
 end;
 

--- a/src/Pure/Isar/specification.ML	Fri Oct 02 20:51:32 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Oct 02 21:39:06 2009 +0200
@@ -286,7 +286,7 @@
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
         val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
-      in ((prems, stmt, []), goal_ctxt) end
+      in ((prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
@@ -327,7 +327,7 @@
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
-      in ((prems, stmt, facts), goal_ctxt) end);
+      in ((prems, stmt, SOME facts), goal_ctxt) end);
 
 structure TheoremHook = GenericDataFun
 (
@@ -372,7 +372,7 @@
       [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
-    |> Proof.refine_insert facts
+    |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
   end;