# HG changeset patch
# User blanchet
# Date 1406928823 -7200
# Node ID 5ef0531d9db2f5f74bbee9b7d915c833558ad3c2
# Parent  a63f14f1214c4b2685b4c2e74bc01295ded66f02
tweaked 'clone' formula detection

diff -r a63f14f1214c -r 5ef0531d9db2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 23:29:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 23:33:43 2014 +0200
@@ -109,7 +109,7 @@
          is_before_skolemize_rule () then
         add_lines_pass2 (line :: res) t lines
       else
-        add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
+        add_lines_pass2 res prev_t (map (replace_dependencies_in_line (name, deps)) lines)
     end
 
 type isar_params =
@@ -159,8 +159,7 @@
           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
 
         val atp_proof =
-          atp_proof
-          |> rpair [] |-> fold_rev add_line_pass1
+          fold_rev add_line_pass1 atp_proof []
           |> add_lines_pass2 [] Term.dummy
 
         val conjs =