--- 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;