# HG changeset patch
# User wenzelm
# Date 1165353282 -3600
# Node ID 5e31241e1e3cf581c06b5c65516e7ca3bbc9bc9f
# Parent  2a0c0fa4a3c430e631045acce570b5fe1808bc65
Attrib.internal: morphism;

diff -r 2a0c0fa4a3c4 -r 5e31241e1e3c src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Dec 05 22:14:41 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Dec 05 22:14:42 2006 +0100
@@ -59,7 +59,7 @@
 
       fun add_for_f fname psimps =
         note_theorem
-          ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts),
+          ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
             psimps) #> snd
     in
       (saved_psimps,
@@ -78,8 +78,11 @@
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
             |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
-            ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
-            ||>> PROFILE "adding termination" (note_theorem ((qualify "termination", []), [termination]))
+            ||>> PROFILE "adding pinduct"
+              (note_theorem ((qualify "pinduct",
+                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
+            ||>> PROFILE "adding termination"
+              (note_theorem ((qualify "termination", []), [termination]))
             ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
             ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
 
@@ -144,7 +147,7 @@
 
         (* FIXME: How to generate code from (possibly) local contexts*)
       val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-      val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
+      val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
 
       val qualify = NameSpace.qualified defname;
     in
diff -r 2a0c0fa4a3c4 -r 5e31241e1e3c src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Dec 05 22:14:41 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 05 22:14:42 2006 +0100
@@ -677,7 +677,7 @@
       note_theorems
         (map (NameSpace.qualified rec_name) intr_names ~~
          intr_atts ~~
-         map (fn th => [([th], [Attrib.internal (ContextRules.intro_query NONE)])])
+         map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE))])])
            (ProofContext.export ctxt1 ctxt intrs)) |>>
       map (hd o snd); (* FIXME? *)
     val (((_, elims'), (_, [induct'])), ctxt3) =
@@ -685,13 +685,13 @@
       note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
         note_theorem ((NameSpace.qualified (Sign.base_name name) "cases",
-          [Attrib.internal (RuleCases.case_names cases),
-           Attrib.internal (RuleCases.consumes 1),
-           Attrib.internal (InductAttrib.cases_set name),
-           Attrib.internal (ContextRules.elim_query NONE)]), [elim]) #>
+          [Attrib.internal (K (RuleCases.case_names cases)),
+           Attrib.internal (K (RuleCases.consumes 1)),
+           Attrib.internal (K (InductAttrib.cases_set name)),
+           Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) elims ||>>
       note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
-        map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
+        map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
     val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
     val ctxt4 = if no_ind then ctxt3 else
@@ -700,9 +700,9 @@
         ctxt3 |>
         note_theorems [((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), []),
           inducts |> map (fn (name, th) => ([th],
-            [Attrib.internal ind_case_names,
-             Attrib.internal (RuleCases.consumes 1),
-             Attrib.internal (induct_att name)])))] |> snd
+            [Attrib.internal (K ind_case_names),
+             Attrib.internal (K (RuleCases.consumes 1)),
+             Attrib.internal (K (induct_att name))])))] |> snd
       end;
 
     val names = map #1 cnames_syn;
diff -r 2a0c0fa4a3c4 -r 5e31241e1e3c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:41 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:42 2006 +0100
@@ -35,7 +35,7 @@
     attribute * (Context.generic * Args.T list)) -> src -> attribute
   val no_args: attribute -> src -> attribute
   val add_del_args: attribute -> attribute -> src -> attribute
-  val internal: attribute -> src
+  val internal: (morphism -> attribute) -> src
 end;
 
 structure Attrib: ATTRIB =
@@ -267,7 +267,8 @@
 
 fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
 
-fun internal_att x = syntax (Scan.lift Args.internal_attribute) x;
+fun internal_att x =
+  syntax (Scan.lift Args.internal_attribute >> (fn att => att Morphism.identity)) x;
 
 
 (* theory setup *)
diff -r 2a0c0fa4a3c4 -r 5e31241e1e3c src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Dec 05 22:14:41 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Dec 05 22:14:42 2006 +0100
@@ -241,7 +241,7 @@
             |>> (fn [(_, [th])] => th)
           end;
 
-        val atts = map Attrib.internal
+        val atts = map (Attrib.internal o K)
           [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
         val prems = subtract_prems loc_ctxt elems_ctxt;
         val stmt = [(("", atts), [(thesis, [])])];