src/HOL/Nominal/Examples/Crary.thy

--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -627,11 +627,7 @@
 apply (force)
 apply (rule ty_cases)
 done
-
-termination
-apply(relation "measure (\<lambda>(_,_,_,T). size T)")
-apply(auto)
-done
+termination by lexicographic_order
 
 lemma logical_monotonicity:
  fixes \<Gamma> \<Gamma>' :: Ctxt