src/Pure/Isar/method.ML

--- a/src/Pure/Isar/method.ML	Mon Jun 29 16:07:55 2015 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jun 29 19:27:07 2015 +0200
@@ -69,6 +69,7 @@
   val closure: bool Config.T
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val detect_closure_state: thm -> bool
+  val STATIC: (unit -> unit) -> cases_tactic
   val RUNTIME: cases_tactic -> cases_tactic
   val sleep: Time.time -> cases_tactic
   val evaluate: text -> Proof.context -> method
@@ -434,13 +435,16 @@
   method ctxt;
 
 
-(* closure vs. runtime state *)
+(* static vs. runtime state *)
 
 fun detect_closure_state st =
   (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) st)) of
     NONE => false
   | SOME t => Term.is_dummy_pattern t);
 
+fun STATIC test st =
+  if detect_closure_state st then (test (); Seq.single ([], st)) else Seq.empty;
+
 fun RUNTIME (tac: cases_tactic) st =
   if detect_closure_state st then Seq.empty else tac st;
 
@@ -696,9 +700,12 @@
           val _ =
             (case drop (Thm.nprems_of st) names of
               [] => ()
-            | bad => (* FIXME Seq.Error *)
-                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
-                  Position.here (Position.set_range (Token.range_of bad))));
+            | 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" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))