1.1 --- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:53:21 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:20 2010 +0200
     1.3 @@ -7,14 +7,13 @@
     1.4  theory Groebner_Basis
     1.5  imports Numeral_Simprocs Nat_Transfer
     1.6  uses
     1.7 -  "Tools/Groebner_Basis/normalizer_data.ML"
     1.8    "Tools/Groebner_Basis/normalizer.ML"
     1.9    ("Tools/Groebner_Basis/groebner.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Semiring normalization *}
    1.13  
    1.14 -setup NormalizerData.setup
    1.15 +setup Normalizer.setup
    1.16  
    1.17  locale gb_semiring =
    1.18    fixes add mul pwr r0 r1
    1.19 @@ -203,7 +202,7 @@
    1.20  in
    1.21  
    1.22  fun normalizer_funs key =
    1.23 -  NormalizerData.funs key
    1.24 +  Normalizer.funs key
    1.25     {is_const = fn phi => numeral_is_const,
    1.26      dest_const = fn phi => fn ct =>
    1.27        Rat.rat_of_int (snd
    1.28 @@ -217,7 +216,6 @@
    1.29  
    1.30  declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
    1.31  
    1.32 -
    1.33  locale gb_ring = gb_semiring +
    1.34    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.35      and neg :: "'a \<Rightarrow> 'a"
    1.36 @@ -246,14 +244,6 @@
    1.37  
    1.38  declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
    1.39  
    1.40 -use "Tools/Groebner_Basis/normalizer.ML"
    1.41 -
    1.42 -
    1.43 -method_setup sring_norm = {*
    1.44 -  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
    1.45 -*} "semiring normalizer"
    1.46 -
    1.47 -
    1.48  locale gb_field = gb_ring +
    1.49    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.50      and inverse:: "'a \<Rightarrow> 'a"
    1.51 @@ -421,6 +411,7 @@
    1.52      "P \<equiv> False \<Longrightarrow> \<not> P"
    1.53      "\<not> P \<Longrightarrow> (P \<equiv> False)"
    1.54    by auto
    1.55 +
    1.56  use "Tools/Groebner_Basis/groebner.ML"
    1.57  
    1.58  method_setup algebra =
    1.59 @@ -674,7 +665,7 @@
    1.60  in
    1.61   val field_comp_conv = comp_conv;
    1.62   val fieldgb_declaration = 
    1.63 -  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
    1.64 +  Normalizer.funs @{thm class_fieldgb.fieldgb_axioms'}
    1.65     {is_const = K numeral_is_const,
    1.66      dest_const = K dest_const,
    1.67      mk_const = mk_const,