updated Eisbach, using version fb741500f533 of its Bitbucket repository;

--- a/src/HOL/Eisbach/Eisbach.thy	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Sun May 03 18:51:26 2015 +0200
@@ -1,11 +1,11 @@
-(*  Title:      Eisbach.thy
+(*  Title:      HOL/Eisbach/Eisbach.thy
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Main entry point for Eisbach proof method language.
 *)
 
 theory Eisbach
-imports Pure
+imports Main
 keywords
   "method" :: thy_decl and
   "conclusion"
@@ -16,7 +16,6 @@
   "uses"
 begin
 
-
 ML_file "parse_tools.ML"
 ML_file "eisbach_rule_insts.ML"
 ML_file "method_closure.ML"
@@ -24,20 +23,12 @@
 ML_file "eisbach_antiquotations.ML"
 
 (* FIXME reform Isabelle/Pure attributes to make this work by default *)
-attribute_setup THEN =
-  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) =>
-    Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
-  "resolution with rule"
-
-attribute_setup OF =
-  \<open>Attrib.thms >> (fn Bs =>
-    Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
-  "rule resolved with facts"
-
-attribute_setup rotated =
-  \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n =>
-    Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
-  "rotated theorem premises"
+setup \<open>
+  fold (Method_Closure.wrap_attribute true)
+    [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
+  fold (Method_Closure.wrap_attribute false)
+    [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
+\<close>
 
 method solves methods m = (m; fail)
 

--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Eisbach_Tools.thy
+(*  Title:      HOL/Eisbach/Eisbach_Tools.thy
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Usability tools for Eisbach.

--- a/src/HOL/Eisbach/Examples.thy	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/Examples.thy	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Examples.thy
+(*  Title:      HOL/Eisbach/Examples.thy
     Author:     Daniel Matichuk, NICTA/UNSW
 *)
 

--- a/src/HOL/Eisbach/Tests.thy	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tests.thy
+(*  Title:      HOL/Eisbach/Tests.thy
     Author:     Daniel Matichuk, NICTA/UNSW
 *)
 
@@ -9,6 +9,7 @@
 begin
 
 
+
 section \<open>Named Theorems Tests\<close>
 
 named_theorems foo
@@ -161,6 +162,7 @@
 
 end
 
+
 (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
    by retrofitting. This needs to be done more carefully to avoid smashing
    legitimate pairs.*)
@@ -292,7 +294,7 @@
   done
 
 
-ML {*
+ML \<open>
 structure Data = Generic_Data
 (
   type T = thm list;
@@ -300,7 +302,7 @@
   val extend = I;
   fun merge data : T = Thm.merge_thms data;
 );
-*}
+\<close>
 
 local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close>
 
@@ -321,6 +323,34 @@
 
 end
 
+
+notepad begin
+  fix A x
+  assume X: "\<And>x. A x"
+  have "A x"
+  by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
+
+  fix A x B
+  assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
+  assume Y: "A B"
+  have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
+  apply (intro conjI)
+  apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
+  apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
+  apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
+  apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
+  apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
+  apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)  
+  done
+  
+  fix x :: "prop" and A
+  assume X: "TERM x"
+  assume Y: "\<And>x :: prop. A x"
+  have "A TERM x"
+  apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
+  done
+end
+
 (* Method name internalization test *)
 
 method test2 = (simp)

--- a/src/HOL/Eisbach/eisbach_antiquotations.ML	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_antiquotations.ML	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      eisbach_antiquotations.ML
+(*  Title:      HOL/Eisbach/eisbach_antiquotations.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 ML antiquotations for Eisbach.

--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      eisbach_rule_insts.ML
+(*  Title:      HOL/Eisbach/eisbach_rule_insts.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Eisbach-aware variants of the "where" and "of" attributes.
@@ -77,10 +77,11 @@
   Named_Insts of ((indexname * string) * (term -> unit)) list
 | Term_Insts of (indexname * term) list;
 
-fun embed_indexname ((xi,s),f) =
+fun embed_indexname ((xi, s), f) =
   let
-    fun wrap_xi xi t = Logic.mk_conjunction (Logic.mk_term (Var (xi,fastype_of t)),Logic.mk_term t);
-  in ((xi,s),f o wrap_xi xi) end;
+    fun wrap_xi xi t =
+      Logic.mk_conjunction (Logic.mk_term (Var (xi, fastype_of t)), Logic.mk_term t);
+  in ((xi, s), f o wrap_xi xi) end;
 
 fun unembed_indexname t =
   let
@@ -98,9 +99,9 @@
 
     val insts' =
       if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
-      then Term_Insts (map (fn (_,t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
+      then Term_Insts (map (fn (_, t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
       else Named_Insts (map (fn (xi, p) => embed_indexname
-            ((xi,Parse_Tools.the_parse_val p),Parse_Tools.the_parse_fun p)) insts);
+            ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts);
   in
     (insts', fixes)
   end;
@@ -132,13 +133,14 @@
       if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
       then
         Term_Insts
-          (map_filter (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
-
+          (map_filter
+            (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
       else
         Named_Insts
-          (apply2 (map (Option.map (fn p => (Parse_Tools.the_parse_val p,Parse_Tools.the_parse_fun p))))
+          (apply2
+            (map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
             (insts, concl_insts)
-            |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
+          |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
   in
     (insts', fixes)
   end;

--- a/src/HOL/Eisbach/match_method.ML	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      match_method.ML
+(*  Title:      HOL/Eisbach/match_method.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Setup for "match" proof method. It provides basic fact/term matching in
@@ -61,8 +61,8 @@
 
 val fixes =
   Parse.and_list1 (Scan.repeat1  (Parse.position bound_term) --
-    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs))
-  >> flat;
+    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ)
+    >> (fn (xs, T) => map (fn (nm, pos) => ((nm, T), pos)) xs)) >> flat;
 
 val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
 
@@ -89,7 +89,6 @@
         | "cut" => {multi = multi, cut = true}))
       ss {multi = false, cut = false});
 
-(*TODO: Shape holes in thms *)
 fun parse_named_pats match_kind =
   Args.context :|-- (fn ctxt =>
     Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :--
@@ -105,20 +104,18 @@
       SOME (Token.Source src) =>
         let
           val text = Method_Closure.read_inner_method ctxt src
-          (*TODO: Correct parse context for attributes?*)
           val ts' =
             map
               (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
                 ((Option.map (fn (b, att) =>
-                  (Parse_Tools.the_real_val b,
-                    map (Attrib.attribute ctxt) att)) b, match_args), v)
+                  (Parse_Tools.the_real_val b, att)) b, match_args), v)
                 | _ => raise Fail "Expected closed term") ts
-          val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes
+          val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes
         in (ts', fixes', text) end
     | SOME _ => error "Unexpected token value in match cartouche"
     | NONE =>
         let
-          val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
+          val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
           val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
           val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
 
@@ -135,9 +132,11 @@
 
           val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
 
-          val _ = map2 (fn nm => fn (_,pos) => member (op =) pat_fixes nm orelse
-            error ("For-fixed variable must be bound in some pattern." ^ Position.here pos))
-            fix_nms fixes;
+          val _ =
+            map2 (fn nm => fn (_, pos) =>
+                member (op =) pat_fixes nm orelse
+                error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
+              fix_nms fixes;
 
           val _ = map (Term.map_types Type.no_tvars) pats
 
@@ -164,20 +163,27 @@
 
                   val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
                     |> Conjunction.intr_balanced
-                    |> Drule.generalize ([], map fst abs_nms);
+                    |> Drule.generalize ([], map fst abs_nms)
+                    |> Method_Closure.tag_free_thm;
 
-                  val thm =
+                  val atts = map (Attrib.attribute ctxt') att;
+                  val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
+
+                  fun label_thm thm =
                     Thm.cterm_of ctxt' (Free (nm, propT))
                     |> Drule.mk_term
-                    |> not (null abs_nms) ? Conjunction.intr param_thm
-                    |> Drule.zero_var_indexes
-                    |> Method_Closure.tag_free_thm;
+                    |> not (null abs_nms) ? Conjunction.intr thm
+
+                  val [head_thm, body_thm] =
+                    Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm'])
+                    |> map Method_Closure.tag_free_thm;
 
-                  (*TODO: Preprocess attributes here?*)
-
-                  val (_, ctxt'') = Proof_Context.note_thmss "" [((b, []), [([thm], [])])] ctxt';
+                  val ctxt''' =
+                    Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt''
+                    |> snd
+                    |> Variable.declare_maxidx (Thm.maxidx_of head_thm);
                 in
-                  (SOME (Thm.prop_of thm, map (Attrib.attribute ctxt) att) :: tms, ctxt'')
+                  (SOME (Thm.prop_of head_thm, att) :: tms, ctxt''')
                 end
             | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
 
@@ -196,7 +202,20 @@
           val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
           val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats');
 
-          val binds' = map (Option.map (fn (t, atts) => (Morphism.term morphism t, atts))) binds;
+          fun close_src src =
+            let
+              val src' = Token.closure_src src |> Token.transform_src morphism;
+              val _ =
+                map2 (fn tok1 => fn tok2 =>
+                  (case (Token.get_value tok2) of
+                    SOME value => Token.assign (SOME value) tok1
+                  | NONE => ()))
+                  (Token.args_of_src src)
+                  (Token.args_of_src src');
+            in src' end;
+
+          val binds' =
+            map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds;
 
           val _ =
             ListPair.app
@@ -207,7 +226,8 @@
 
           val real_fixes' = map (Morphism.term morphism) real_fixes;
           val _ =
-            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes');
+            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f), _) , _), t) => f t)
+              (fixes, real_fixes');
 
           val match_args = map (fn (_, (_, match_args)) => match_args) ts;
           val binds'' = (binds' ~~ match_args) ~~ pats';
@@ -247,36 +267,30 @@
         (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
           | _ => NONE) fact_insts';
 
-    fun apply_attribute thm att ctxt =
-      let
-        val (opt_context', thm') = att (Context.Proof ctxt, thm)
-      in
-        (case thm' of
-          SOME _ => error "Rule attributes cannot be applied here"
-        | _ => the_default ctxt (Option.map Context.proof_of opt_context'))
-      end;
-
-    fun apply_attributes atts thm = fold (apply_attribute thm) atts;
-
-     (*TODO: What to do about attributes that raise errors?*)
-    val (fact_insts, ctxt') =
-      fold_map (fn (head, (thms, atts : attribute list)) => fn ctxt =>
-        ((head, thms), fold (apply_attributes atts) thms ctxt)) fact_insts ctxt;
-
     fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm;
 
-    fun expand_fact thm =
+    fun expand_fact fact_insts thm =
       the_default [thm]
         (case try_dest_term thm of
           SOME t_ident => AList.lookup (op aconv) fact_insts t_ident
         | NONE => NONE);
 
-    val morphism =
+    fun fact_morphism fact_insts =
       Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
       Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
-      Morphism.fact_morphism "do_inst.fact" (maps expand_fact);
+      Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts));
 
-    val text' = Method.map_source (Token.transform_src morphism) text;
+    fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) =
+      let
+        val morphism = fact_morphism fact_insts;
+        val atts' = map (Attrib.attribute ctxt o Token.transform_src morphism) atts;
+        val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt;
+      in ((head, fact'') :: fact_insts, ctxt') end;
+
+     (*TODO: What to do about attributes that raise errors?*)
+    val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt);
+
+    val text' = Method.map_source (Token.transform_src (fact_morphism fact_insts')) text;
   in
     (text', ctxt')
   end;
@@ -304,27 +318,27 @@
   let
     val tenv = Envir.term_env env;
     val tyenv = Envir.type_env env;
-    val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
-    val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
+    val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
+    val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
   in
     Envir.Envir
-      {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env),
+      {maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env),
         tenv = tenv, tyenv = tyenv}
   end
 
 fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
   let
     val tenv = Envir.term_env inner_env
-      |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t)));
+      |> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t)));
 
     val tyenv = Envir.type_env inner_env
-      |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T)));
+      |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
 
     val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
 
     val param_vars = map Term.dest_Var params;
 
-    val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
+    val params' = map (fn (xi, _) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
 
     val fixes_vars = map Term.dest_Var fixes;
 
@@ -339,11 +353,11 @@
       Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
       |> recalculate_maxidx;
 
-    val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params';
+    val all_params_bound = forall (fn SOME (_, Var _) => true | _ => false) params';
 
     val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
 
-    val all_pat_fixes_bound = forall (fn (xi,_) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
+    val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
 
     val thm' = Morphism.thm morphism thm;
 
@@ -469,7 +483,7 @@
       SOME (x, seq') =>
         if member eq prev x
         then Seq.pull (deduplicate eq prev seq')
-        else SOME (x,deduplicate eq (x :: prev) seq')
+        else SOME (x, deduplicate eq (x :: prev) seq')
     | NONE => NONE));
 
 fun consistent_env env =
@@ -480,7 +494,7 @@
     forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
   end;
 
-fun eq_env (env1,env2) =
+fun eq_env (env1, env2) =
   let
     val tyenv1 = Envir.type_env env1;
     val tyenv2 = Envir.type_env env2;
@@ -492,7 +506,7 @@
           Envir.eta_contract (Envir.norm_term env2 t')))
       (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
     andalso
-    ListPair.allEq (fn ((var, (_, T)), (var', (_,T'))) =>
+    ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
         var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
       (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
   end;
@@ -505,15 +519,13 @@
 
     fun match_thm (((x, params), pat), thm) env  =
       let
-        fun try_dest_term term = the_default term (try Logic.dest_term term);
-
         val pat_vars = Term.add_vars pat [];
 
-        val pat' = pat |> Envir.norm_term env |> try_dest_term;
+        val pat' = pat |> Envir.norm_term env;
 
-        val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt
+        val (((Tinsts', insts), [thm']), inner_ctxt) = Variable.import false [thm] ctxt;
 
-        val item' = Thm.prop_of thm' |> try_dest_term;
+        val item' = Thm.prop_of thm';
 
         val ts = Option.map (fst o fst) (fst x);
 
@@ -572,7 +584,6 @@
         |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt')
       end;
 
-    (*TODO: Slightly hacky re-use of fact match implementation in plain term matching *)
     fun make_term_matches ctxt get =
       let
         val pats' =

--- a/src/HOL/Eisbach/method_closure.ML	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      method_closure.ML
+(*  Title:      HOL/Eisbach/method_closure.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Facilities for treating method syntax as a closure, with abstraction
@@ -13,6 +13,7 @@
   val is_dummy: thm -> bool
   val tag_free_thm: thm -> thm
   val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
+  val wrap_attribute: bool -> Binding.binding -> theory -> theory
   val read_inner_method: Proof.context -> Token.src -> Method.text
   val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text
   val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text
@@ -35,12 +36,10 @@
 
 structure Data = Generic_Data
 (
-  type T =
-    ((term list * (string list * string list)) * Method.text) Symtab.table;
+  type T = ((term list * (string list * string list)) * Method.text) Symtab.table;
   val empty: T = Symtab.empty;
   val extend = I;
-  fun merge (methods1,methods2) : T =
-    (Symtab.merge (K true) (methods1, methods2));
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 val get_methods = Data.get o Context.Proof;
@@ -88,6 +87,32 @@
     if exists is_free_thm (thm :: args) then dummy_free_thm
     else f context thm);
 
+fun free_aware_attribute thy declaration src (context, thm) =
+  let
+    val src' = Token.init_assignable_src src;
+    fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
+    val _ = try apply_att Drule.dummy_thm;
+    val src'' = Token.closure_src src';
+    val thms =
+      map_filter Token.get_value (Token.args_of_src src'')
+      |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
+      |> flat;
+  in
+    if exists is_free_thm (thm :: thms) then
+      if declaration then (NONE, NONE)
+      else (NONE, SOME dummy_free_thm)
+    else apply_att thm
+  end;
+
+fun wrap_attribute declaration binding thy =
+  let
+    val name = Binding.name_of binding;
+    val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
+    fun get_src src = Token.src (name', Token.range_of_src src) (Token.args_of_src src);
+  in
+    Attrib.define_global binding (free_aware_attribute thy declaration o get_src) "" thy
+    |> snd
+  end;
 
 (* thm semantics for combined methods with internal parser. Simulates outer syntax parsing. *)
 (* Creates closures for each combined method while parsing, based on the parse context *)
@@ -108,7 +133,8 @@
     val method_text = read_inner_method ctxt src;
     val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
     (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *)
-    val _ = Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
+    val _ = Method.map_source (fn src =>
+                  (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
     val src' = Token.closure_src src;
   in (src', method_text') end;
 
@@ -127,7 +153,7 @@
       NONE =>
         let
            val input = Token.input_of tok;
-           val (src,text) = read_inner_text_closure ctxt input;
+           val (src, text) = read_inner_text_closure ctxt input;
            val _ = Token.assign (SOME (Token.Source src)) tok;
         in text end
     | SOME (Token.Source src) => read_inner_method ctxt src

--- a/src/HOL/Eisbach/parse_tools.ML	Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML	Sun May 03 18:51:26 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      parse_tools.ML
+(*  Title:      HOL/Eisbach/parse_tools.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Simple tools for deferred stateful token values.