# HG changeset patch
# User wenzelm
# Date 1452694174 -3600
# Node ID dca35981c8fb3f155802cd6ae95de13ec537db0a
# Parent  9aa4012fc45dd50bf822ac94d2b9b6b69945dfaa
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);

diff -r 9aa4012fc45d -r dca35981c8fb src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Wed Jan 13 09:38:24 2016 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Wed Jan 13 15:09:34 2016 +0100
@@ -204,8 +204,8 @@
         (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
         >> (fn args =>
             let val args' = read_where_insts args in
-              Thm.mixed_attribute (fn (context, thm) =>
-                (context, read_instantiate_closed (Context.proof_of context) args' thm))
+              fn (context, thm) =>
+                (NONE, SOME (read_instantiate_closed (Context.proof_of context) args' thm))
             end))
       "named instantiation of theorem");
 
@@ -221,12 +221,12 @@
         let
           val read_insts = read_of_insts (not unchecked) context args;
         in
-          Thm.mixed_attribute (fn (context, thm) =>
+          fn (context, thm) =>
             let val thm' =
               if Thm.is_free_dummy thm andalso unchecked
               then Drule.free_dummy_thm
               else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
-            in (context, thm') end)
+            in (NONE, SOME thm') end
         end))
       "positional instantiation of theorem");