# HG changeset patch
# User wenzelm
# Date 1376681616 -7200
# Node ID 8cbfbeb566a4c5e5c4b042fd3dbcdf19ba157897
# Parent  aa0322a65bea5f378c2823058db6179cc5c02f2f
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;

diff -r aa0322a65bea -r 8cbfbeb566a4 src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:28:05 2013 +0200
+++ b/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:33:36 2013 +0200
@@ -46,10 +46,24 @@
 
 ML_file "measurable.ML"
 
-attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
-attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
-attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
-method_setup measurable = {* Measurable.method *} "measurability prover"
+attribute_setup measurable = {*
+  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+    Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
+    (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
+*} "declaration of measurability theorems"
+
+attribute_setup measurable_dest = {*
+  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
+*} "add dest rule for measurability prover"
+
+attribute_setup measurable_app = {*
+  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
+*} "add application rule for measurability prover"
+
+method_setup measurable = {*
+  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
+*} "measurability prover"
+
 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
 
 declare
diff -r aa0322a65bea -r 8cbfbeb566a4 src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Fri Aug 16 21:28:05 2013 +0200
+++ b/src/HOL/Probability/measurable.ML	Fri Aug 16 21:33:36 2013 +0200
@@ -8,13 +8,13 @@
 sig
   datatype level = Concrete | Generic
 
-  val simproc : Proof.context -> cterm -> thm option
-  val method : (Proof.context -> Method.method) context_parser
+  val add_app : thm -> Context.generic -> Context.generic
+  val add_dest : thm -> Context.generic -> Context.generic
+  val add_thm : bool * level -> thm -> Context.generic -> Context.generic
+
   val measurable_tac : Proof.context -> thm list -> tactic
 
-  val attr : attribute context_parser
-  val dest_attr : attribute context_parser
-  val app_attr : attribute context_parser
+  val simproc : Proof.context -> cterm -> thm option
 
   val get : level -> Proof.context -> thm list
   val get_all : Proof.context -> thm list
@@ -213,21 +213,6 @@
 fun measurable_tac ctxt facts =
   TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
 
-val attr_add = Thm.declaration_attribute o add_thm;
-
-val attr : attribute context_parser =
-  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
-     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
-
-val dest_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
-
-val app_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
-
-val method : (Proof.context -> Method.method) context_parser =
-  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
-
 fun simproc ctxt redex =
   let
     val t = HOLogic.mk_Trueprop (term_of redex);