# HG changeset patch
# User bulwahn
# Date 1287681188 -7200
# Node ID 638ce4dabe53759cb50f29896b5e02c26d1436c0
# Parent  75d9f57123d688acea457ddd77c3c91b8ed6ff77
for now safely but unpractically assume no predicate is terminating

diff -r 75d9f57123d6 -r 638ce4dabe53 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:08 2010 +0200
@@ -1982,7 +1982,7 @@
 
 fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val is_terminating = true (* FIXME: requires an termination analysis *)  
+    val is_terminating = false (* FIXME: requires an termination analysis *)  
     val compilation_modifiers =
       (if pol then compilation_modifiers else
         negative_comp_modifiers_of compilation_modifiers)