# HG changeset patch
# User blanchet
# Date 1343050350 -7200
# Node ID 67a6bcbd358728000818ed8a0e252eaa04eb80c5
# Parent  3e45c98fe127464cee94bdcc4cfd7d983450c713
removed MaSh junk arising from primrec definitions

diff -r 3e45c98fe127 -r 67a6bcbd3587 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
@@ -719,11 +719,13 @@
       let
         val all_names =
           facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
-        val deps_of =
-          if atp then
-            atp_dependencies_of ctxt params prover auto_level facts all_names
+        fun deps_of status th =
+          if status = Non_Rec_Def orelse status = Rec_Def then
+            SOME []
+          else if atp then
+            atp_dependencies_of ctxt params prover auto_level facts all_names th
           else
-            isar_dependencies_of all_names
+            isar_dependencies_of all_names th
         fun do_commit [] [] state = state
           | do_commit adds reps {fact_G} =
             let
@@ -751,13 +753,13 @@
            else
              ())
         fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
-          | learn_new_fact ((_, stature), th)
+          | learn_new_fact ((_, stature as (_, status)), th)
                            (adds, (parents, n, next_commit, _)) =
             let
               val name = nickname_of th
               val feats =
                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
-              val deps = deps_of th |> these
+              val deps = deps_of status th |> these
               val n = n |> not (null deps) ? Integer.add 1
               val adds = (name, parents, feats, deps) :: adds
               val (adds, next_commit) =
@@ -783,11 +785,12 @@
                 |> fold learn_new_fact new_facts
             in commit true adds []; n end
         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
-          | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
+          | relearn_old_fact ((_, (_, status)), th)
+                             (reps, (n, next_commit, _)) =
             let
               val name = nickname_of th
               val (n, reps) =
-                case deps_of th of
+                case deps_of status th of
                   SOME deps => (n + 1, (name, deps) :: reps)
                 | NONE => (n, reps)
               val (reps, next_commit) =