--- a/src/HOL/Tools/Function/termination.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/termination.ML Fri Dec 02 14:54:25 2011 +0100
@@ -182,7 +182,7 @@
(case try @{const_name Orderings.less_eq} of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+ if prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
then False thm2 else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match
@@ -260,7 +260,7 @@
val pT = HOLogic.mk_prodT (T, T)
val n = length qs
val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
- val conds' = if null conds then [HOLogic.true_const] else conds
+ val conds' = if null conds then [@{term True}] else conds
in
HOLogic.Collect_const pT $
Abs ("uu_", pT,