src/HOL/Tools/function_package/fundef_package.ML
changeset 21658 5e31241e1e3c
parent 21602 cb13024d0e36
child 22102 a89ef7144729
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Dec 05 22:14:41 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Dec 05 22:14:42 2006 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5        fun add_for_f fname psimps =
     1.6          note_theorem
     1.7 -          ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts),
     1.8 +          ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
     1.9              psimps) #> snd
    1.10      in
    1.11        (saved_psimps,
    1.12 @@ -78,8 +78,11 @@
    1.13        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.14            lthy
    1.15              |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    1.16 -            ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    1.17 -            ||>> PROFILE "adding termination" (note_theorem ((qualify "termination", []), [termination]))
    1.18 +            ||>> PROFILE "adding pinduct"
    1.19 +              (note_theorem ((qualify "pinduct",
    1.20 +                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
    1.21 +            ||>> PROFILE "adding termination"
    1.22 +              (note_theorem ((qualify "termination", []), [termination]))
    1.23              ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
    1.24              ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
    1.25  
    1.26 @@ -144,7 +147,7 @@
    1.27  
    1.28          (* FIXME: How to generate code from (possibly) local contexts*)
    1.29        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    1.30 -      val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    1.31 +      val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
    1.32  
    1.33        val qualify = NameSpace.qualified defname;
    1.34      in