--- a/src/HOL/Tools/Function/lexicographic_order.ML Tue Oct 05 16:33:16 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Tue Oct 05 18:09:29 2010 +0200
@@ -119,14 +119,17 @@
(** Proof Reconstruction **)
(* prove row :: cell list -> tactic *)
-fun prove_row (Less less_thm :: _) =
- (rtac @{thm "mlex_less"} 1)
- THEN PRIMITIVE (Thm.elim_implies less_thm)
- | prove_row (LessEq (lesseq_thm, _) :: tail) =
- (rtac @{thm "mlex_leq"} 1)
- THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
- THEN prove_row tail
- | prove_row _ = sys_error "lexicographic_order"
+fun prove_row (c :: cs) =
+ (case Lazy.force c of
+ Less thm =>
+ rtac @{thm "mlex_less"} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ | LessEq (thm, _) =>
+ rtac @{thm "mlex_leq"} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ THEN prove_row cs
+ | _ => sys_error "lexicographic_order")
+ | prove_row [] = no_tac;
(** Error reporting **)
@@ -200,7 +203,6 @@
| SOME order =>
let
val clean_table = map (fn x => map (nth x) order) table
- |> map (map Lazy.force)
val relation = mk_measures domT (map (nth measure_funs) order)
val _ = if not quiet
then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))