# HG changeset patch
# User krauss
# Date 1262470738 -3600
# Node ID f66bb6536f6a65a13d04feb1e8e2e295fa2abffc
# Parent  bc0cea4cae52fb674959ea0acce9a5d4b6e82a81
simplified

diff -r bc0cea4cae52 -r f66bb6536f6a src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -194,32 +194,36 @@
   | dest_call D t = error "dest_call"
 
 
-fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
+fun mk_desc thy tac vs Gam l r m1 m2 =
+  let
+    fun try rel =
+      try_proof (cterm_of thy
+        (Term.list_all (vs,
+           Logic.mk_implies (HOLogic.mk_Trueprop Gam,
+             HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+               $ (m2 $ r) $ (m1 $ l)))))) tac
+  in
+    case try @{const_name HOL.less} of
+       Solved thm => Less thm
+     | Stuck thm =>
+       (case try @{const_name HOL.less_eq} of
+          Solved thm2 => LessEq (thm2, thm)
+        | Stuck thm2 =>
+          if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+          then False thm2 else None (thm2, thm)
+        | _ => raise Match) (* FIXME *)
+     | _ => raise Match
+end
+
+fun derive_descent thy tac c m1 m2 D =
   case get_descent D c m1 m2 of
     SOME _ => D
-  | NONE => let
-    fun cgoal rel =
-      Term.list_all (vs,
-        Logic.mk_implies (HOLogic.mk_Trueprop Gam,
-          HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
-            $ (m2 $ r') $ (m1 $ l'))))
-      |> cterm_of thy
-    in
-      note_descent c m1 m2
-        (case try_proof (cgoal @{const_name HOL.less}) tac of
-           Solved thm => Less thm
-         | Stuck thm =>
-           (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
-              Solved thm2 => LessEq (thm2, thm)
-            | Stuck thm2 =>
-              if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
-              then False thm2 else None (thm2, thm)
-            | _ => raise Match) (* FIXME *)
-         | _ => raise Match) D
-      end
-
-fun derive_descent thy tac c m1 m2 D =
-  derive_desc_aux thy tac c (dest_call D c) m1 m2 D
+  | NONE => 
+    let
+      val (vs, _, l, _, r, Gam) = dest_call D c
+    in 
+      note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
+    end
 
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st