# HG changeset patch
# User wenzelm
# Date 1460023991 -7200
# Node ID fdc290b68ecd9792d43deceebbea8c6883ba0bf7
# Parent  8093203f0b895f1e3de529e51ec8c1423a1bb745
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);

diff -r 8093203f0b89 -r fdc290b68ecd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Apr 07 12:08:02 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Apr 07 12:13:11 2016 +0200
@@ -500,7 +500,78 @@
 (* theory setup *)
 
 val _ = Theory.setup
- (register_config Goal.quick_and_dirty_raw #>
+ (setup @{binding tagged} (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
+  setup @{binding untagged} (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
+  setup @{binding kind} (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
+  setup @{binding THEN}
+    (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
+      >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B))))
+    "resolution with rule" #>
+  setup @{binding OF}
+    (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs)))
+    "rule resolved with facts" #>
+  setup @{binding rename_abs}
+    (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
+      Thm.rule_attribute [] (K (Drule.rename_bvars' vs))))
+    "rename bound variables in abstractions" #>
+  setup @{binding unfolded}
+    (thms >> (fn ths =>
+      Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths)))
+    "unfolded definitions" #>
+  setup @{binding folded}
+    (thms >> (fn ths =>
+      Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths)))
+    "folded definitions" #>
+  setup @{binding consumes}
+    (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
+    "number of consumed facts" #>
+  setup @{binding constraints}
+    (Scan.lift Parse.nat >> Rule_Cases.constraints)
+    "number of equality constraints" #>
+  setup @{binding case_names}
+    (Scan.lift (Scan.repeat1 (Args.name --
+      Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []))
+      >> (fn cs =>
+        Rule_Cases.cases_hyp_names
+          (map #1 cs)
+          (map (map (the_default Rule_Cases.case_hypsN) o #2) cs)))
+    "named rule cases" #>
+  setup @{binding case_conclusion}
+    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
+    "named conclusion of rule cases" #>
+  setup @{binding params}
+    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
+    "named rule parameters" #>
+  setup @{binding rule_format}
+    (Scan.lift (Args.mode "no_asm")
+      >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format))
+    "result put into canonical rule format" #>
+  setup @{binding elim_format}
+    (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
+    "destruct rule turned into elimination rule format" #>
+  setup @{binding no_vars}
+    (Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
+      let
+        val ctxt = Variable.set_body false (Context.proof_of context);
+        val ((_, [th']), _) = Variable.import true [th] ctxt;
+      in th' end)))
+    "imported schematic variables" #>
+  setup @{binding atomize}
+    (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
+  setup @{binding rulify}
+    (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #>
+  setup @{binding rotated}
+    (Scan.lift (Scan.optional Parse.int 1
+      >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #>
+  setup @{binding defn}
+    (add_del Local_Defs.defn_add Local_Defs.defn_del)
+    "declaration of definitional transformations" #>
+  setup @{binding abs_def}
+    (Scan.succeed (Thm.rule_attribute [] (fn context =>
+      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+    "abstract over free variables of definitional theorem" #>
+
+  register_config Goal.quick_and_dirty_raw #>
   register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
   register_config Printer.show_brackets_raw #>
diff -r 8093203f0b89 -r fdc290b68ecd src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 07 12:08:02 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 07 12:13:11 2016 +0200
@@ -1281,109 +1281,6 @@
 in end\<close>
 
 
-section \<open>Isar attributes\<close>
-
-attribute_setup tagged =
-  \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
-  "tagged theorem"
-
-attribute_setup untagged =
-  \<open>Scan.lift Args.name >> Thm.untag\<close>
-  "untagged theorem"
-
-attribute_setup kind =
-  \<open>Scan.lift Args.name >> Thm.kind\<close>
-  "theorem kind"
-
-attribute_setup THEN =
-  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
-    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
-  "resolution with rule"
-
-attribute_setup OF =
-  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
-  "rule resolved with facts"
-
-attribute_setup rename_abs =
-  \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
-    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
-  "rename bound variables in abstractions"
-
-attribute_setup unfolded =
-  \<open>Attrib.thms >> (fn ths =>
-    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
-  "unfolded definitions"
-
-attribute_setup folded =
-  \<open>Attrib.thms >> (fn ths =>
-    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
-  "folded definitions"
-
-attribute_setup consumes =
-  \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
-  "number of consumed facts"
-
-attribute_setup constraints =
-  \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
-  "number of equality constraints"
-
-attribute_setup case_names =
-  \<open>Scan.lift (Scan.repeat1 (Args.name --
-    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
-    >> (fn cs =>
-      Rule_Cases.cases_hyp_names
-        (map #1 cs)
-        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close>
-  "named rule cases"
-
-attribute_setup case_conclusion =
-  \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
-  "named conclusion of rule cases"
-
-attribute_setup params =
-  \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
-  "named rule parameters"
-
-attribute_setup rule_format =
-  \<open>Scan.lift (Args.mode "no_asm")
-    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
-  "result put into canonical rule format"
-
-attribute_setup elim_format =
-  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
-  "destruct rule turned into elimination rule format"
-
-attribute_setup no_vars =
-  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
-    let
-      val ctxt = Variable.set_body false (Context.proof_of context);
-      val ((_, [th']), _) = Variable.import true [th] ctxt;
-    in th' end))\<close>
-  "imported schematic variables"
-
-attribute_setup atomize =
-  \<open>Scan.succeed Object_Logic.declare_atomize\<close>
-  "declaration of atomize rule"
-
-attribute_setup rulify =
-  \<open>Scan.succeed Object_Logic.declare_rulify\<close>
-  "declaration of rulify rule"
-
-attribute_setup rotated =
-  \<open>Scan.lift (Scan.optional Parse.int 1
-    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
-  "rotated theorem premises"
-
-attribute_setup defn =
-  \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
-  "declaration of definitional transformations"
-
-attribute_setup abs_def =
-  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
-    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
-  "abstract over free variables of definitional theorem"
-
-
 section \<open>Further content for the Pure theory\<close>
 
 subsection \<open>Meta-level connectives in assumptions\<close>