# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID f765c323405975101260ff5f4fb5ee59f984b495
# Parent  4785ef554dccdc104a469f8e5f7f2e25a03f837b
changed proof method to handle widen predicate in JinjaThreads

diff -r 4785ef554dcc -r f765c3234059 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -1926,11 +1926,11 @@
         (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ 
           "splitting with rules \n" ^
         commas (map (Display.string_of_thm_global thy) split_rules)))
-        THEN (Splitter.split_asm_tac split_rules 1)
+        THEN TRY ((Splitter.split_asm_tac split_rules 1)
         THEN (print_tac "after splitting with split_asm rules")
         (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
           THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
-        THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
+          THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
         THEN (assert_tac (Max_number_of_subgoals 2))
         THEN (EVERY (map split_term_tac ts))
       end