# HG changeset patch
# User blanchet
# Date 1394791545 -3600
# Node ID ae164dc4b2a1883c03f08100f404eb7183e9a4d9
# Parent  fc937e7ef4c64c7b79b613793206d4d13438a0b6
debugging stuff

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