# HG changeset patch
# User wenzelm
# Date 1442148243 -7200
# Node ID 2a03ae772c60ccfd478201d363bdea216dda559a
# Parent  c94c65f35d01c1198f1d5c3dce0cb24df38ec4cd
method "goals" ignores facts;

diff -r c94c65f35d01 -r 2a03ae772c60 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 14:42:34 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 14:44:03 2015 +0200
@@ -886,10 +886,10 @@
   method; thus a plain \emph{do-nothing} proof step would be ``@{command
   "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
 
-  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} is like ``@{method "-"}'', but
-  the current subgoals are turned into cases within the context (see also
-  \secref{sec:cases-induct}). The specified case names are used if present;
-  otherwise cases are numbered starting from 1.
+  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
+  into cases within the context (see also \secref{sec:cases-induct}). The
+  specified case names are used if present; otherwise cases are numbered
+  starting from 1.
 
   Invoking cases in the subsequent proof body via the @{command_ref case}
   command will @{command fix} goal parameters, @{command assume} goal
diff -r c94c65f35d01 -r 2a03ae772c60 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Sep 13 14:42:34 2015 +0200
+++ b/src/Pure/Isar/method.ML	Sun Sep 13 14:44:03 2015 +0200
@@ -694,20 +694,19 @@
   setup @{binding "-"} (Scan.succeed (K insert_facts))
     "insert current facts, nothing else" #>
   setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
-    METHOD_CASES (fn facts =>
-      Seq.THEN (ALLGOALS (insert_tac facts), fn st =>
-        let
-          val _ =
-            (case drop (Thm.nprems_of st) names of
-              [] => ()
-            | bad =>
-                if detect_closure_state st then ()
-                else
-                  (* FIXME Seq.Error *)
-                  error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
-                    Position.here (Position.set_range (Token.range_of bad))));
-        in goals_tac ctxt (map Token.content_of names) st end))))
-    "insert facts and bind cases for goals" #>
+    METHOD_CASES (fn facts => fn st =>
+      let
+        val _ =
+          (case drop (Thm.nprems_of st) names of
+            [] => ()
+          | bad =>
+              if detect_closure_state st then ()
+              else
+                (* FIXME Seq.Error *)
+                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+                  Position.here (Position.set_range (Token.range_of bad))));
+      in goals_tac ctxt (map Token.content_of names) st end)))
+    "bind cases for goals" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts" #>
   setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))