# HG changeset patch
# User blanchet
# Date 1376916467 -7200
# Node ID 877f5c28016f9d716b3079713da24a59f5b489f5
# Parent  019ecbb18e3f04672bde7ece18bef43ebd6247a7
add subtypes as well as features in MaSh

diff -r 019ecbb18e3f -r 877f5c28016f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 14:41:22 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 14:47:47 2013 +0200
@@ -616,6 +616,8 @@
     fun add_type T =
       add_type_pats type_max_depth T
       #> fold_atyps_sorts (fn (_, S) => add_classes S) T
+    fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
+      | add_subtypes T = add_type T
 
     fun pattify_term _ 0 _ = []
       | pattify_term args _ (Const (x as (s, _))) =
@@ -640,24 +642,23 @@
         add_term_pat feature_of depth t
         #> add_term_pats feature_of (depth - 1) t
     fun add_term feature_of = add_term_pats feature_of term_max_depth
-
-    fun add_pats t =
+    fun add_subterms t =
       case strip_comb t of
         (Const (x as (_, T)), args) =>
         let val (built_in, args) = is_built_in x args in
           (not built_in ? add_term const_feature_of t)
-          #> add_type T
-          #> fold add_pats args
+          #> add_subtypes T
+          #> fold add_subterms args
         end
       | (head, args) =>
         (case head of
-           Const (_, T) => add_term const_feature_of t #> add_type T
-         | Free (_, T) => add_term free_feature_of t #> add_type T
-         | Var (_, T) => add_type T
-         | Abs (_, T, body) => add_type T #> add_pats body
+           Const (_, T) => add_term const_feature_of t #> add_subtypes T
+         | Free (_, T) => add_term free_feature_of t #> add_subtypes T
+         | Var (_, T) => add_subtypes T
+         | Abs (_, T, body) => add_subtypes T #> add_subterms body
          | _ => I)
-        #> fold add_pats args
-  in [] |> fold add_pats ts end
+        #> fold add_subterms args
+  in [] |> fold add_subterms ts end
 
 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})