# HG changeset patch
# User wenzelm
# Date 1434992147 -7200
# Node ID 86fc6652c4df1db5cf90e3ab3195faa1f245bd7e
# Parent  742b553d88b2b159d1f2e1df3958430af29acb9d
tuned signature;

diff -r 742b553d88b2 -r 86fc6652c4df src/HOL/Eisbach/Eisbach_Tools.thy
--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Mon Jun 22 17:44:43 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Mon Jun 22 18:55:47 2015 +0200
@@ -14,7 +14,8 @@
 fun trace_method parser print =
   Scan.lift (Args.mode "dummy") -- parser >>
     (fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
-      (if dummy orelse not (Method_Closure.is_dummy st) then tracing (print ctxt x) else ();
+      (if dummy orelse not (Method.detect_closure_state st)
+       then tracing (print ctxt x) else ();
        all_tac st)));
 
 fun setup_trace_method binding parser print =
diff -r 742b553d88b2 -r 86fc6652c4df src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Mon Jun 22 17:44:43 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Mon Jun 22 18:55:47 2015 +0200
@@ -791,9 +791,8 @@
 val match_parser =
   parse_match_kind :-- (fn kind =>
       Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
-    (fn (matches, bodies) => fn ctxt => fn using => fn goal =>
-      if Method_Closure.is_dummy goal then Seq.empty
-      else
+    (fn (matches, bodies) => fn ctxt => fn using =>
+      Method.RUNTIME (fn st =>
         let
           fun exec (pats, fixes, text) goal =
             let
@@ -801,7 +800,7 @@
                 fold Variable.declare_term fixes ctxt
                 |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
             in real_match using ctxt' fixes matches text pats goal end;
-        in Seq.flat (Seq.FIRST (map exec bodies) goal) end);
+        in Seq.flat (Seq.FIRST (map exec bodies) st) end));
 
 val _ =
   Theory.setup
diff -r 742b553d88b2 -r 86fc6652c4df src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Mon Jun 22 17:44:43 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Mon Jun 22 18:55:47 2015 +0200
@@ -10,7 +10,6 @@
 
 signature METHOD_CLOSURE =
 sig
-  val is_dummy: thm -> bool
   val tag_free_thm: thm -> thm
   val is_free_thm: thm -> bool
   val dummy_free_thm: thm
@@ -71,11 +70,6 @@
 
 (* free thm *)
 
-fun is_dummy thm =
-  (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) thm)) of
-    NONE => false
-  | SOME t => Term.is_dummy_pattern t);
-
 val free_thmN = "Method_Closure.free_thm";
 fun tag_free_thm thm = Thm.tag_rule (free_thmN, "") thm;
 
@@ -233,12 +227,9 @@
           Token.Fact (SOME name, evaluate_dynamic_thm ctxt name)
       | x => x);
 
-fun method_evaluate text ctxt : Method.method = fn facts => fn st =>
-  let
-    val ctxt' = Config.put Method.closure false ctxt;
-  in
-    if is_dummy st then Seq.empty
-    else Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st
+fun method_evaluate text ctxt facts =
+  let val ctxt' = Config.put Method.closure false ctxt in
+    Method.RUNTIME (fn st => Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st)
   end;
 
 fun evaluate_method_def fix_env raw_text ctxt =
diff -r 742b553d88b2 -r 86fc6652c4df src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jun 22 17:44:43 2015 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jun 22 18:55:47 2015 +0200
@@ -67,6 +67,8 @@
   val method_closure: Proof.context -> Token.src -> Token.src
   val closure: bool Config.T
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
+  val detect_closure_state: thm -> bool
+  val RUNTIME: cases_tactic -> cases_tactic
   val evaluate: text -> Proof.context -> method
   type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
   val modifier: attribute -> Position.T -> modifier
@@ -419,6 +421,17 @@
   method ctxt;
 
 
+(* closure 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 RUNTIME (tac: cases_tactic) st =
+  if detect_closure_state st then Seq.empty else tac st;
+
+
 (* evaluate method text *)
 
 local