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 @@ -320,7 +320,7 @@
     1.4  val atp_dependency_default_max_fact = 50
     1.5  
     1.6  (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
     1.7 -val typedef_sig = [@{thm CollectI} |> nickname_of]
     1.8 +val typedef_deps = [@{thm CollectI} |> nickname_of]
     1.9  
    1.10  (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
    1.11  val typedef_ths =
    1.12 @@ -332,15 +332,24 @@
    1.13           type_definition.Abs_image}
    1.14    |> map nickname_of
    1.15  
    1.16 -fun trim_dependencies deps =
    1.17 -  if length deps > max_dependencies orelse deps = typedef_sig orelse
    1.18 -     exists (member (op =) typedef_ths) deps then
    1.19 +fun is_size_def [dep] th =
    1.20 +    (case first_field ".recs" dep of
    1.21 +       SOME (pref, _) =>
    1.22 +       (case first_field ".size" (nickname_of th) of
    1.23 +          SOME (pref', _) => pref = pref'
    1.24 +        | NONE => false)
    1.25 +     | NONE => false)
    1.26 +  | is_size_def _ _ = false
    1.27 +
    1.28 +fun trim_dependencies th deps =
    1.29 +  if length deps > max_dependencies orelse deps = typedef_deps orelse
    1.30 +     exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
    1.31      NONE
    1.32    else
    1.33      SOME deps
    1.34  
    1.35 -fun isar_dependencies_of all_names =
    1.36 -  thms_in_proof (SOME all_names) #> trim_dependencies
    1.37 +fun isar_dependencies_of all_names th =
    1.38 +  th |> thms_in_proof (SOME all_names) |> trim_dependencies th
    1.39  
    1.40  fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
    1.41                          auto_level facts all_names th =
    1.42 @@ -386,7 +395,7 @@
    1.43             end
    1.44           else
    1.45             ();
    1.46 -         used_facts |> map fst |> trim_dependencies)
    1.47 +         used_facts |> map fst |> trim_dependencies th)
    1.48        | _ => NONE
    1.49      end
    1.50