--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:15:46 2014 +0100
@@ -89,9 +89,6 @@
fun add_lines_pass2 res [] = rev res
| add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
let
-val line as (name, role, t, rule, deps) = (name, role, Term.map_aterms
- (perhaps (try (fn Free (s, T) => Free (unsuffix "__" s, T)))) t
- |> Term.map_abs_vars (perhaps (try (unsuffix "__"))), rule, deps) (*###*)
val is_last_line = null lines
fun looks_interesting () =