src/HOL/Algebra/ringsimp.ML

--- a/src/HOL/Algebra/ringsimp.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Mon May 07 00:49:59 2007 +0200
@@ -20,9 +20,8 @@
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
-structure AlgebraData = GenericDataFun
-(struct
-  val name = "Algebra/algebra";
+structure Data = GenericDataFun
+(
   type T = ((string * term list) * thm list) list;
     (* Algebraic structures:
        identifier of the structure, list of operations and simp rules,
@@ -30,20 +29,16 @@
   val empty = [];
   val extend = I;
   fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
-  fun print generic structs =
-    let
-      val ctxt = Context.proof_of generic;
-      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
-      fun pretty_struct ((s, ts), _) = Pretty.block
-        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
-         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
-    in
-      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
-        Pretty.writeln
-    end
-end);
+);
 
-val print_structures = AlgebraData.print o Context.Proof;
+fun print_structures ctxt =
+  let
+    val structs = Data.get (Context.Proof ctxt);
+    val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    fun pretty_struct ((s, ts), _) = Pretty.block
+      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
+       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
+  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
 
 
 (** Method **)
@@ -57,17 +52,17 @@
   in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
 
 fun algebra_tac ctxt =
-  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
+  EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
 
 
 (** Attribute **)
 
 fun add_struct_thm s =
   Thm.declaration_attribute
-    (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+    (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
 fun del_struct s =
   Thm.declaration_attribute
-    (fn _ => AlgebraData.map (AList.delete struct_eq s));
+    (fn _ => Data.map (AList.delete struct_eq s));
 
 val attribute = Attrib.syntax
      (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
@@ -79,7 +74,6 @@
 (** Setup **)
 
 val setup =
-  AlgebraData.init #>
   Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
     "normalisation of algebraic structure")] #>
   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];