diff -r ae50c9b82444 -r e87974cd9b86 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Tue Feb 17 17:22:45 2015 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Wed Feb 18 22:46:47 2015 +0100
@@ -72,10 +72,6 @@
 context comm_semiring_1
 begin
 
-lemma normalizing_semiring_ops:
-  shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
-    and "TERM 0" and "TERM 1" .
-
 lemma normalizing_semiring_rules:
   "(a * m) + (b * m) = (a + b) * m"
   "(a * m) + m = (a + 1) * m"
@@ -116,85 +112,65 @@
   by (simp_all add: algebra_simps power_add power2_eq_square
     power_mult_distrib power_mult del: one_add_one)
 
-lemmas normalizing_comm_semiring_1_axioms =
-  comm_semiring_1_axioms [normalizer
-    semiring ops: normalizing_semiring_ops
-    semiring rules: normalizing_semiring_rules]
+declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
+  {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
+    @{thms normalizing_semiring_rules}), ring = ([], []), field = ([], []), idom = [], ideal = []}\<close>
 
 end
 
 context comm_ring_1
 begin
 
-lemma normalizing_ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
-
 lemma normalizing_ring_rules:
   "- x = (- 1) * x"
   "x - y = x + (- y)"
   by simp_all
 
-lemmas normalizing_comm_ring_1_axioms =
-  comm_ring_1_axioms [normalizer
-    semiring ops: normalizing_semiring_ops
-    semiring rules: normalizing_semiring_rules
-    ring ops: normalizing_ring_ops
-    ring rules: normalizing_ring_rules]
+declaration \<open>Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
+  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
+    ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], @{thms normalizing_ring_rules}), field = ([], []), idom = [], ideal = []}\<close>
 
 end
 
 context comm_semiring_1_cancel_crossproduct
 begin
 
-lemmas
-  normalizing_comm_semiring_1_cancel_crossproduct_axioms =
-  comm_semiring_1_cancel_crossproduct_axioms [normalizer
-    semiring ops: normalizing_semiring_ops
-    semiring rules: normalizing_semiring_rules
-    idom rules: crossproduct_noteq add_scale_eq_noteq]
+declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms}
+  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
+    ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\<close>
 
 end
 
 context idom
 begin
 
-lemmas normalizing_idom_axioms = idom_axioms [normalizer
-  semiring ops: normalizing_semiring_ops
-  semiring rules: normalizing_semiring_rules
-  ring ops: normalizing_ring_ops
-  ring rules: normalizing_ring_rules
-  idom rules: crossproduct_noteq add_scale_eq_noteq
-  ideal rules: right_minus_eq add_0_iff]
+declaration \<open>Semiring_Normalizer.declare @{thm idom_axioms}
+  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms},
+    ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms},
+    field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq},
+    ideal = @{thms right_minus_eq add_0_iff}}\<close>
 
 end
 
 context field
 begin
 
-lemma normalizing_field_ops:
-  shows "TERM (x / y)" and "TERM (inverse x)" .
-
 lemmas normalizing_field_rules = divide_inverse inverse_eq_divide
 
-lemmas normalizing_field_axioms =
-  field_axioms [normalizer
-    semiring ops: normalizing_semiring_ops
-    semiring rules: normalizing_semiring_rules
-    ring ops: normalizing_ring_ops
-    ring rules: normalizing_ring_rules
-    field ops: normalizing_field_ops
-    field rules: normalizing_field_rules
-    idom rules: crossproduct_noteq add_scale_eq_noteq
-    ideal rules: right_minus_eq add_0_iff]
+declaration \<open>Semiring_Normalizer.declare @{thm field_axioms}
+  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms},
+    ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms},
+    field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms normalizing_field_rules}),
+    idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms},
+    ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close>
 
 end
 
-hide_fact (open) normalizing_comm_semiring_1_axioms
-  normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules
+hide_fact (open) normalizing_semiring_rules
 
-hide_fact (open) normalizing_comm_ring_1_axioms
-  normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
+hide_fact (open) normalizing_ring_rules
 
-hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
+hide_fact (open) normalizing_field_rules
 
 code_identifier
   code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith