--- 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
--- 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