self-contained declaration attribute

--- a/src/HOL/Semiring_Normalization.thy	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -122,9 +122,6 @@
     semiring ops: normalizing_semiring_ops
     semiring rules: normalizing_semiring_rules]
 
-declaration
-  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
-
 end
 
 context comm_ring_1
@@ -144,9 +141,6 @@
     ring ops: normalizing_ring_ops
     ring rules: normalizing_ring_rules]
 
-declaration
-  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
-
 end
 
 context comm_semiring_1_cancel_crossproduct
@@ -162,9 +156,6 @@
     semiring rules: normalizing_semiring_rules
     idom rules: crossproduct_noteq add_scale_eq_noteq]
 
-declaration
-  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_crossproduct_axioms} *}
-
 end
 
 context idom
@@ -180,9 +171,6 @@
   idom rules: crossproduct_noteq add_scale_eq_noteq
   ideal rules: right_minus_eq add_0_iff]
 
-declaration
-  {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
-
 end
 
 context field
@@ -204,9 +192,6 @@
     idom rules: crossproduct_noteq add_scale_eq_noteq
     ideal rules: right_minus_eq add_0_iff]
 
-declaration
-  {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
-
 end
 
 hide_fact (open) normalizing_comm_semiring_1_axioms

--- a/src/HOL/Tools/semiring_normalizer.ML	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Feb 15 17:01:22 2015 +0100
@@ -12,8 +12,6 @@
   val del: attribute
   val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
     field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
-  val semiring_funs: thm -> declaration
-  val field_funs: thm -> declaration
 
   val semiring_normalize_conv: Proof.context -> conv
   val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
@@ -101,32 +99,31 @@
   
   (* extra-logical functions *)
 
-fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
+fun funs key {is_const, dest_const, mk_const, conv} = 
  Data.map (fn data =>
   let
-    val key = Morphism.thm phi raw_key;
     val _ = AList.defined Thm.eq_thm data key orelse
       raise THM ("No data entry for structure key", 0, [key]);
-    val fns = {is_const = is_const phi, dest_const = dest_const phi,
-      mk_const = mk_const phi, conv = conv phi};
+    val fns = {is_const = is_const, dest_const = dest_const,
+      mk_const = mk_const, conv = conv};
   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
 
 val semiring_norm_ss =
   simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms semiring_norm});
 
-fun semiring_funs raw_key = funs raw_key
-   {is_const = K (can HOLogic.dest_number o Thm.term_of),
-    dest_const = K (fn ct =>
+fun semiring_funs key = funs key
+   {is_const = can HOLogic.dest_number o Thm.term_of,
+    dest_const = (fn ct =>
       Rat.rat_of_int (snd
         (HOLogic.dest_number (Thm.term_of ct)
           handle TERM _ => error "ring_dest_const"))),
-    mk_const = K (fn cT => fn x => Numeral.mk_cnumber cT
+    mk_const = (fn cT => fn x => Numeral.mk_cnumber cT
       (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int")),
-    conv = K (fn ctxt =>
+    conv = (fn ctxt =>
       Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
       then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1}))};
 
-fun field_funs raw_key =
+fun field_funs key =
   let
     fun numeral_is_const ct =
       case term_of ct of
@@ -149,11 +146,11 @@
                          (Numeral.mk_cnumber cT a))
              (Numeral.mk_cnumber cT b)
       end
-  in funs raw_key
-     {is_const = K numeral_is_const,
-      dest_const = K dest_const,
-      mk_const = K mk_const,
-      conv = K Numeral_Simprocs.field_comp_conv}
+  in funs key
+     {is_const = numeral_is_const,
+      dest_const = dest_const,
+      mk_const = mk_const,
+      conv = Numeral_Simprocs.field_comp_conv}
   end;
 
 
@@ -215,7 +212,8 @@
         ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'},
           {is_const = undefined, dest_const = undefined, mk_const = undefined,
           conv = undefined}))
-    end)
+    end
+    |> (if null f_ops then semiring_funs else field_funs) key)
 
 
 (** auxiliary **)

--- a/src/HOL/ex/Groebner_Examples.thy	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -5,7 +5,7 @@
 section {* Groebner Basis Examples *}
 
 theory Groebner_Examples
-imports Groebner_Basis
+imports "~~/src/HOL/Groebner_Basis"
 begin
 
 subsection {* Basic examples *}