1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:05:44 2014 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:05:45 2014 +0100
1.3 @@ -89,6 +89,9 @@
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 () =