# HG changeset patch
# User wenzelm
# Date 1135207746 -3600
# Node ID 180c99dfbad45e314aa4c1c179bcb5312212fe11
# Parent  8bf56053475a48cb8a393398cff3d735b4821902
conjunction_tac: single goal;

diff -r 8bf56053475a -r 180c99dfbad4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Dec 22 00:29:04 2005 +0100
+++ b/src/Pure/Isar/method.ML	Thu Dec 22 00:29:06 2005 +0100
@@ -141,10 +141,9 @@
 fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
 
 fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
-  Seq.THEN (TRY Tactic.conjunction_tac, tac facts));
+  Seq.THEN (ALLGOALS Tactic.conjunction_tac, tac facts));
 
-fun METHOD tac = RAW_METHOD (fn facts =>
-  TRY Tactic.conjunction_tac THEN tac facts);
+fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Tactic.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);