# HG changeset patch
# User blanchet
# Date 1355778388 -3600
# Node ID 681edd111e9b0de89af54c15dab84dc7ee18c296
# Parent  001a0e12d7f1eaf936e97ce4bf2ecc05bcab1617
really honor pattern depth, and use 2 by default

diff -r 001a0e12d7f1 -r 681edd111e9b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
@@ -542,7 +542,7 @@
       | do_add_type (TFree (_, S)) = add_classes S
       | do_add_type (TVar (_, S)) = add_classes S
     fun add_type T = type_max_depth >= 0 ? do_add_type T
-    fun patternify_term _ ~1 _ = []
+    fun patternify_term _ 0 _ = []
       | patternify_term args _ (Const (x as (s, _))) =
         if is_bad_const x args then [] else [s]
       | patternify_term _ depth (Free (s, _)) =
@@ -550,7 +550,6 @@
           [thy_name ^ Long_Name.separator ^ s]
         else
           []
-      | patternify_term _ 0 _ = []
       | patternify_term args depth (t $ u) =
         let
           val ps = patternify_term (u :: args) depth t
@@ -559,7 +558,7 @@
       | patternify_term _ _ _ = []
     fun add_term_pattern feature_of =
       union (op = o pairself fst) o map feature_of oo patternify_term []
-    fun add_term_patterns _ ~1 _ = I
+    fun add_term_patterns _ 0 _ = I
       | add_term_patterns feature_of depth t =
         add_term_pattern feature_of depth t
         #> add_term_patterns feature_of (depth - 1) t
@@ -578,8 +577,8 @@
 
 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
 
-val term_max_depth = 1
-val type_max_depth = 1
+val term_max_depth = 2
+val type_max_depth = 2
 
 (* TODO: Generate type classes for types? *)
 fun features_of ctxt prover thy (scope, status) ts =