# HG changeset patch
# User wenzelm
# Date 1135207744 -3600
# Node ID 8bf56053475a48cb8a393398cff3d735b4821902
# Parent  255eaf0a2119b0dd99f2773751636b24831195d3
CONJUNCTS2;

diff -r 255eaf0a2119 -r 8bf56053475a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 22 00:29:03 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Dec 22 00:29:04 2005 +0100
@@ -2110,7 +2110,7 @@
 
 val refine_protected =
   Proof.refine (Method.Basic (K (Method.RAW_METHOD
-    (K (ALLGOALS (CONJUNCTS (ALLGOALS (Tactic.rtac Drule.protectI))))))))
+    (K (ALLGOALS (CONJUNCTS2 ~1 (ALLGOALS (Tactic.rtac Drule.protectI))))))))
   #> Seq.hd;
 
 fun goal_name thy kind target propss =