diff -r 1b3115d1a8df -r 8d8c70b41bab src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -74,17 +74,17 @@
       handle TERM _ => [];
 
     val prems = ProofContext.prems_of ctxt;
-    val rings = flat (map (ring_filter o #prop o rep_thm) prems);
-    val comms = flat (map (comm_filter o #prop o rep_thm) prems);
+    val rings = List.concat (map (ring_filter o #prop o rep_thm) prems);
+    val comms = List.concat (map (comm_filter o #prop o rep_thm) prems);
     val non_comm_rings = rings \\ comms;
     val comm_rings = rings inter_string comms;
     val _ = tracing
       ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
        "\nCommutative rings in proof context: " ^ commas comm_rings);
     val simps =
-      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", NONE))
+      List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", NONE))
         non_comm_rings) @
-      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", NONE))
+      List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", NONE))
         comm_rings);
   in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
   end;