src/Pure/Proof/extraction.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18921 f47c46d7d654
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -355,7 +355,7 @@
     1.4  
     1.5  (** expanding theorems / definitions **)
     1.6  
     1.7 -fun add_expand_thm (thy, thm) =
     1.8 +fun add_expand_thm thm thy =
     1.9    let
    1.10      val {realizes_eqns, typeof_eqns, types, realizers,
    1.11        defs, expand, prep} = ExtractionData.get thy;
    1.12 @@ -379,10 +379,13 @@
    1.13        else
    1.14          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    1.15           realizers = realizers, defs = defs,
    1.16 -         expand = (name, prop_of thm) ins expand, prep = prep}) thy, thm)
    1.17 +         expand = (name, prop_of thm) ins expand, prep = prep}) thy)
    1.18    end;
    1.19  
    1.20 -fun add_expand_thms thms thy = Library.foldl (fst o add_expand_thm) (thy, thms);
    1.21 +val add_expand_thms = fold add_expand_thm;
    1.22 +
    1.23 +val extraction_expand =
    1.24 +  Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm));
    1.25  
    1.26  
    1.27  (** types with computational content **)
    1.28 @@ -445,8 +448,7 @@
    1.29      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    1.30  
    1.31     Attrib.add_attributes
    1.32 -     [("extraction_expand",
    1.33 -       (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
    1.34 +     [("extraction_expand", extraction_expand,
    1.35         "specify theorems / definitions to be expanded during extraction")]);
    1.36  
    1.37