1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -719,11 +719,13 @@
     1.4        let
     1.5          val all_names =
     1.6            facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
     1.7 -        val deps_of =
     1.8 -          if atp then
     1.9 -            atp_dependencies_of ctxt params prover auto_level facts all_names
    1.10 +        fun deps_of status th =
    1.11 +          if status = Non_Rec_Def orelse status = Rec_Def then
    1.12 +            SOME []
    1.13 +          else if atp then
    1.14 +            atp_dependencies_of ctxt params prover auto_level facts all_names th
    1.15            else
    1.16 -            isar_dependencies_of all_names
    1.17 +            isar_dependencies_of all_names th
    1.18          fun do_commit [] [] state = state
    1.19            | do_commit adds reps {fact_G} =
    1.20              let
    1.21 @@ -751,13 +753,13 @@
    1.22             else
    1.23               ())
    1.24          fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
    1.25 -          | learn_new_fact ((_, stature), th)
    1.26 +          | learn_new_fact ((_, stature as (_, status)), th)
    1.27                             (adds, (parents, n, next_commit, _)) =
    1.28              let
    1.29                val name = nickname_of th
    1.30                val feats =
    1.31                  features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    1.32 -              val deps = deps_of th |> these
    1.33 +              val deps = deps_of status th |> these
    1.34                val n = n |> not (null deps) ? Integer.add 1
    1.35                val adds = (name, parents, feats, deps) :: adds
    1.36                val (adds, next_commit) =
    1.37 @@ -783,11 +785,12 @@
    1.38                  |> fold learn_new_fact new_facts
    1.39              in commit true adds []; n end
    1.40          fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
    1.41 -          | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
    1.42 +          | relearn_old_fact ((_, (_, status)), th)
    1.43 +                             (reps, (n, next_commit, _)) =
    1.44              let
    1.45                val name = nickname_of th
    1.46                val (n, reps) =
    1.47 -                case deps_of th of
    1.48 +                case deps_of status th of
    1.49                    SOME deps => (n + 1, (name, deps) :: reps)
    1.50                  | NONE => (n, reps)
    1.51                val (reps, next_commit) =