Attrib.internal: morphism;
authorwenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 216585e31241e1e3c
parent 21657 2a0c0fa4a3c4
child 21659 b8531e5164f0
Attrib.internal: morphism;
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/specification.ML
     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
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Dec 05 22:14:41 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 05 22:14:42 2006 +0100
     2.3 @@ -677,7 +677,7 @@
     2.4        note_theorems
     2.5          (map (NameSpace.qualified rec_name) intr_names ~~
     2.6           intr_atts ~~
     2.7 -         map (fn th => [([th], [Attrib.internal (ContextRules.intro_query NONE)])])
     2.8 +         map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE))])])
     2.9             (ProofContext.export ctxt1 ctxt intrs)) |>>
    2.10        map (hd o snd); (* FIXME? *)
    2.11      val (((_, elims'), (_, [induct'])), ctxt3) =
    2.12 @@ -685,13 +685,13 @@
    2.13        note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
    2.14        fold_map (fn (name, (elim, cases)) =>
    2.15          note_theorem ((NameSpace.qualified (Sign.base_name name) "cases",
    2.16 -          [Attrib.internal (RuleCases.case_names cases),
    2.17 -           Attrib.internal (RuleCases.consumes 1),
    2.18 -           Attrib.internal (InductAttrib.cases_set name),
    2.19 -           Attrib.internal (ContextRules.elim_query NONE)]), [elim]) #>
    2.20 +          [Attrib.internal (K (RuleCases.case_names cases)),
    2.21 +           Attrib.internal (K (RuleCases.consumes 1)),
    2.22 +           Attrib.internal (K (InductAttrib.cases_set name)),
    2.23 +           Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    2.24          apfst (hd o snd)) elims ||>>
    2.25        note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
    2.26 -        map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
    2.27 +        map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    2.28  
    2.29      val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
    2.30      val ctxt4 = if no_ind then ctxt3 else
    2.31 @@ -700,9 +700,9 @@
    2.32          ctxt3 |>
    2.33          note_theorems [((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), []),
    2.34            inducts |> map (fn (name, th) => ([th],
    2.35 -            [Attrib.internal ind_case_names,
    2.36 -             Attrib.internal (RuleCases.consumes 1),
    2.37 -             Attrib.internal (induct_att name)])))] |> snd
    2.38 +            [Attrib.internal (K ind_case_names),
    2.39 +             Attrib.internal (K (RuleCases.consumes 1)),
    2.40 +             Attrib.internal (K (induct_att name))])))] |> snd
    2.41        end;
    2.42  
    2.43      val names = map #1 cnames_syn;
     3.1 --- a/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:41 2006 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:42 2006 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4      attribute * (Context.generic * Args.T list)) -> src -> attribute
     3.5    val no_args: attribute -> src -> attribute
     3.6    val add_del_args: attribute -> attribute -> src -> attribute
     3.7 -  val internal: attribute -> src
     3.8 +  val internal: (morphism -> attribute) -> src
     3.9  end;
    3.10  
    3.11  structure Attrib: ATTRIB =
    3.12 @@ -267,7 +267,8 @@
    3.13  
    3.14  fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
    3.15  
    3.16 -fun internal_att x = syntax (Scan.lift Args.internal_attribute) x;
    3.17 +fun internal_att x =
    3.18 +  syntax (Scan.lift Args.internal_attribute >> (fn att => att Morphism.identity)) x;
    3.19  
    3.20  
    3.21  (* theory setup *)
     4.1 --- a/src/Pure/Isar/specification.ML	Tue Dec 05 22:14:41 2006 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Tue Dec 05 22:14:42 2006 +0100
     4.3 @@ -241,7 +241,7 @@
     4.4              |>> (fn [(_, [th])] => th)
     4.5            end;
     4.6  
     4.7 -        val atts = map Attrib.internal
     4.8 +        val atts = map (Attrib.internal o K)
     4.9            [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
    4.10          val prems = subtract_prems loc_ctxt elems_ctxt;
    4.11          val stmt = [(("", atts), [(thesis, [])])];