# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID c1f86c5d3827a4cc76d16b5f5ca8614036c7aeab
# Parent  d902054e7ac695aba7df956cecd1e8aebbf6c76e
avoiding fishing for split_asm rule in the predicate compiler

diff -r d902054e7ac6 -r c1f86c5d3827 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
@@ -2145,17 +2145,12 @@
           let
             val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
             val num_of_constrs = length (#case_rewrites info)
-            (* special treatment of pairs -- because of fishing *)
-            val split_rules = case (fst o dest_Type o fastype_of) t of
-              "*" => [@{thm prod.split_asm}] 
-              | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
             val (_, ts) = strip_comb t
           in
-            (print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
-              "splitting with rules \n" ^
-            commas (map (Display.string_of_thm ctxt) split_rules)))
-            THEN TRY ((Splitter.split_asm_tac split_rules 1)
-            THEN (print_tac options "after splitting with split_asm rules")
+            print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
+              "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info))
+            THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1)
+              THEN (print_tac options "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)