diff -r 7eed0fee0241 -r 54505623a8ef src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Apr 19 20:01:26 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Apr 20 00:25:05 2014 +0100
@@ -961,7 +961,7 @@
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
+   @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},