src/Pure/Proof/extraction.ML
changeset 18708 4b3dadb4fe33
parent 18358 0a733e11021a
child 18728 6790126ab5f6
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4    fun print _ _ = ();
     1.5  end);
     1.6  
     1.7 -val _ = Context.add_setup [ExtractionData.init];
     1.8 +val _ = Context.add_setup ExtractionData.init;
     1.9  
    1.10  fun read_condeq thy =
    1.11    let val thy' = add_syntax thy
    1.12 @@ -401,7 +401,7 @@
    1.13  (** Pure setup **)
    1.14  
    1.15  val _ = Context.add_setup
    1.16 -  [add_types [("prop", ([], NONE))],
    1.17 +  (add_types [("prop", ([], NONE))] #>
    1.18  
    1.19     add_typeof_eqns
    1.20       ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
    1.21 @@ -422,7 +422,7 @@
    1.22      \    (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
    1.23  
    1.24        "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==>  \
    1.25 -    \    (typeof (f)) == (Type (TYPE('f)))"],
    1.26 +    \    (typeof (f)) == (Type (TYPE('f)))"] #>
    1.27  
    1.28     add_realizes_eqns
    1.29       ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
    1.30 @@ -442,12 +442,12 @@
    1.31      \    (!!x. PROP realizes (Null) (PROP P (x)))",
    1.32  
    1.33        "(realizes (r) (!!x. PROP P (x))) ==  \
    1.34 -    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"],
    1.35 +    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    1.36  
    1.37     Attrib.add_attributes
    1.38       [("extraction_expand",
    1.39         (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
    1.40 -       "specify theorems / definitions to be expanded during extraction")]];
    1.41 +       "specify theorems / definitions to be expanded during extraction")]);
    1.42  
    1.43  
    1.44  (**** extract program ****)