# HG changeset patch
# User wenzelm
# Date 1132406548 -3600
# Node ID c22ee06ac1a7045d703c49a81f104244a1c8854f
# Parent  1945ae1668d20410fca09097e4ab93e7cbbdf61b
CONJUNCTS;

diff -r 1945ae1668d2 -r c22ee06ac1a7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Nov 19 14:21:09 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Nov 19 14:22:28 2005 +0100
@@ -2113,8 +2113,8 @@
   ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
 
 val refine_protected =
-  Proof.refine (Method.Basic (K (Method.METHOD   (* FIXME avoid conjunction_tac (!?) *)
-    (K (ALLGOALS (Tactic.rtac Drule.protectI))))))
+  Proof.refine (Method.Basic (K (Method.RAW_METHOD
+    (K (ALLGOALS (CONJUNCTS (ALLGOALS (Tactic.rtac Drule.protectI))))))))
   #> Seq.hd;
 
 fun goal_name thy kind target propss =