# HG changeset patch
# User blanchet
# Date 1343050350 -7200
# Node ID 9e9b6e363859756eb43a73ddb7caaaebe0ca75fd
# Parent  60759d07df2426f5b6307f8bbc9c50d5ade46538
don't relearn old facts in Isar mode

diff -r 60759d07df24 -r 9e9b6e363859 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -29,7 +29,7 @@
 open Sledgehammer_MaSh
 open Sledgehammer_Run
 
-val cvc3N = "cvc3"
+(* val cvc3N = "cvc3" *)
 val yicesN = "yices"
 val z3N = "z3"
 
diff -r 60759d07df24 -r 9e9b6e363859 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -774,7 +774,7 @@
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
             in (reps, (n, next_commit, timed_out)) end
         val n =
-          if null old_facts then
+          if not atp orelse null old_facts then
             n
           else
             let