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