--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 02 14:54:25 2011 +0100
@@ -79,7 +79,7 @@
(case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
+ if prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2
else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match