--- a/src/HOL/Algebra/ringsimp.ML Fri Mar 14 12:03:23 2003 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 14 18:00:16 2003 +0100
@@ -64,9 +64,9 @@
val cring_ss = HOL_ss settermless termless_ring;
fun cring_normalise ctxt = let
- fun filter t = case HOLogic.dest_Trueprop t of
+ fun filter t = (case HOLogic.dest_Trueprop t of
Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
- | _ => []
+ | _ => [])
handle TERM _ => [];
val insts = flat (map (filter o #prop o rep_thm)
(ProofContext.prems_of ctxt));