diff -r f984f22f1cb4 -r fb080097e436 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Feb 02 16:31:35 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Feb 02 16:31:37 2006 +0100
@@ -36,6 +36,7 @@
   val pretty_goals: bool -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
+  val refine_insert: thm list -> state -> state
   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
   val match_bind: (string list * string) list -> state -> state
   val match_bind_i: (term list * term) list -> state -> state
@@ -422,6 +423,9 @@
 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)));
+
 end;