src/Pure/Proof/extraction.ML
changeset 56206 7adec2a527f5
parent 53171 a5e54d4d9081
child 56239 17df7145a871
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 18 16:16:28 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 18 16:44:51 2014 +0100
     1.3 @@ -466,9 +466,9 @@
     1.4        "(realizes (r) (!!x. PROP P (x))) ==  \
     1.5      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
     1.6  
     1.7 -   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
     1.8 +   Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false))
     1.9       "specify theorems to be expanded during extraction" #>
    1.10 -   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
    1.11 +   Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true))
    1.12       "specify definitions to be expanded during extraction");
    1.13  
    1.14