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