1.1 --- a/src/HOL/Probability/measurable.ML	Fri Aug 16 21:28:05 2013 +0200
     1.2 +++ b/src/HOL/Probability/measurable.ML	Fri Aug 16 21:33:36 2013 +0200
     1.3 @@ -8,13 +8,13 @@
     1.4  sig
     1.5    datatype level = Concrete | Generic
     1.6  
     1.7 -  val simproc : Proof.context -> cterm -> thm option
     1.8 -  val method : (Proof.context -> Method.method) context_parser
     1.9 +  val add_app : thm -> Context.generic -> Context.generic
    1.10 +  val add_dest : thm -> Context.generic -> Context.generic
    1.11 +  val add_thm : bool * level -> thm -> Context.generic -> Context.generic
    1.12 +
    1.13    val measurable_tac : Proof.context -> thm list -> tactic
    1.14  
    1.15 -  val attr : attribute context_parser
    1.16 -  val dest_attr : attribute context_parser
    1.17 -  val app_attr : attribute context_parser
    1.18 +  val simproc : Proof.context -> cterm -> thm option
    1.19  
    1.20    val get : level -> Proof.context -> thm list
    1.21    val get_all : Proof.context -> thm list
    1.22 @@ -213,21 +213,6 @@
    1.23  fun measurable_tac ctxt facts =
    1.24    TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
    1.25  
    1.26 -val attr_add = Thm.declaration_attribute o add_thm;
    1.27 -
    1.28 -val attr : attribute context_parser =
    1.29 -  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    1.30 -     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
    1.31 -
    1.32 -val dest_attr : attribute context_parser =
    1.33 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
    1.34 -
    1.35 -val app_attr : attribute context_parser =
    1.36 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
    1.37 -
    1.38 -val method : (Proof.context -> Method.method) context_parser =
    1.39 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
    1.40 -
    1.41  fun simproc ctxt redex =
    1.42    let
    1.43      val t = HOLogic.mk_Trueprop (term_of redex);