# HG changeset patch
# User blanchet
# Date 1360081153 -3600
# Node ID 242cd1632b0b89a75519e62d0ec8d15aaf1f1b88
# Parent  146f63c3f024fe2ca99e15b4705a7329ac4daa86
removed spurious trimming

diff -r 146f63c3f024 -r 242cd1632b0b src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Feb 04 09:06:20 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Tue Feb 05 17:19:13 2013 +0100
@@ -123,7 +123,7 @@
 fun is_bad_query ctxt ho_atp step j th isar_deps =
   j mod step <> 0 orelse
   Thm.legacy_get_kind th = "" orelse
-  null (these (trim_dependencies th isar_deps)) orelse
+  null isar_deps orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
diff -r 146f63c3f024 -r 242cd1632b0b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 04 09:06:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 05 17:19:13 2013 +0100
@@ -668,9 +668,7 @@
   if length deps > max_dependencies then NONE else SOME deps
 
 fun isar_dependencies_of name_tabs th =
-  let
-    val deps = thms_in_proof (SOME name_tabs) th
-  in
+  let val deps = thms_in_proof (SOME name_tabs) th in
     if deps = [typedef_dep] orelse
        deps = [class_some_dep] orelse
        exists (member (op =) fundef_ths) deps orelse