# HG changeset patch
# User blanchet
# Date 1444124047 -7200
# Node ID 22378817612ff0154044647de584702e29f8f116
# Parent  2007ea8615a2b3698e71f0363ac37f4be0e3b49b
tuning

diff -r 2007ea8615a2 -r 22378817612f src/HOL/Tools/prop_logic.ML
--- 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)