src/HOL/Tools/Groebner_Basis/normalizer.ML

 end
 
 structure Normalizer: NORMALIZER = 
 struct
 
-(* data *)
+(** data **)
 
 type entry =
  {vars: cterm list,
   semiring: cterm list * thm list,
   ring: cterm list * thm list,

   val extend = I;
   val merge = AList.merge Thm.eq_thm (K false);
 );
 
 val get = Data.get o Context.Proof;
-
-
-(* match data *)
 
 fun match ctxt tm =
   let
     fun match_inst
         ({vars, semiring = (sr_ops, sr_rules), 

       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};
   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
 
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
-fun keyword3 k1 k2 k3 =
-  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
-
-val opsN = "ops";
-val rulesN = "rules";
-
-val normN = "norm";
-val constN = "const";
-val delN = "del";
-
-val any_keyword =
-  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
-  keyword2 ringN opsN || keyword2 ringN rulesN ||
-  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
-  keyword2 idomN rulesN || keyword2 idealN rulesN;
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map Drule.dest_term;
-
-fun optional scan = Scan.optional scan [];
-
-in
-
-val normalizer_setup =
-  Attrib.setup @{binding normalizer}
-    (Scan.lift (Args.$$$ delN >> K del) ||
-      ((keyword2 semiringN opsN |-- terms) --
-       (keyword2 semiringN rulesN |-- thms)) --
-      (optional (keyword2 ringN opsN |-- terms) --
-       optional (keyword2 ringN rulesN |-- thms)) --
-      (optional (keyword2 fieldN opsN |-- terms) --
-       optional (keyword2 fieldN rulesN |-- thms)) --
-      optional (keyword2 idomN rulesN |-- thms) --
-      optional (keyword2 idealN rulesN |-- thms)
-      >> (fn ((((sr, r), f), id), idl) => 
-             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
-    "semiring normalizer data";
-
-end;
 
 open Conv;
 
 (* Very basic stuff for terms *)
 

     NONE => reflexive tm
   | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
  
 fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
 
-(* theory setup *)
-
-val setup = normalizer_setup
+
+(** Isar setup **)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
+fun keyword3 k1 k2 k3 =
+  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
+
+val opsN = "ops";
+val rulesN = "rules";
+
+val normN = "norm";
+val constN = "const";
+val delN = "del";
+
+val any_keyword =
+  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
+  keyword2 ringN opsN || keyword2 ringN rulesN ||
+  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
+  keyword2 idomN rulesN || keyword2 idealN rulesN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map Drule.dest_term;
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+val setup =
+  Attrib.setup @{binding normalizer}
+    (Scan.lift (Args.$$$ delN >> K del) ||
+      ((keyword2 semiringN opsN |-- terms) --
+       (keyword2 semiringN rulesN |-- thms)) --
+      (optional (keyword2 ringN opsN |-- terms) --
+       optional (keyword2 ringN rulesN |-- thms)) --
+      (optional (keyword2 fieldN opsN |-- terms) --
+       optional (keyword2 fieldN rulesN |-- thms)) --
+      optional (keyword2 idomN rulesN |-- thms) --
+      optional (keyword2 idealN rulesN |-- thms)
+      >> (fn ((((sr, r), f), id), idl) => 
+             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+    "semiring normalizer data";
 
 end;
+
+end;