--- a/src/HOL/Tools/prop_logic.ML Tue Oct 06 09:27:31 2015 +0200
+++ b/src/HOL/Tools/prop_logic.ML Tue Oct 06 11:34:07 2015 +0200
@@ -316,8 +316,8 @@
(* truth value of a propositional formula 'fm' is computed *)
(* ------------------------------------------------------------------------- *)
-fun eval a True = true
- | eval a False = false
+fun eval _ True = true
+ | eval _ False = false
| eval a (BoolVar i) = (a i)
| eval a (Not fm) = not (eval a fm)
| eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)