--- a/src/HOL/Algebra/ringsimp.ML Mon Jan 24 18:15:19 2005 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Mon Jan 24 18:16:57 2005 +0100
@@ -82,9 +82,9 @@
("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"))
+ flat (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"))
+ flat (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;