# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID 190053ee24edb1baba8b5baf3ee100a8aa656f7c
# Parent  d2261e3141468c9f0edeb913c20d45724f949933
expand type classes into their ancestors for MaSh

diff -r d2261e314146 -r 190053ee24ed src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -516,11 +516,18 @@
 fun interesting_terms_types_and_classes ctxt prover term_max_depth
                                         type_max_depth ts =
   let
+    val thy = Proof_Context.theory_of ctxt
+    val classes = Sign.classes_of thy
     fun is_bad_const (x as (s, _)) args =
       member (op =) logical_consts s orelse
       fst (is_built_in_const_for_prover ctxt prover x args)
     fun add_classes @{sort type} = I
-      | add_classes S = union (op = o pairself fst) (map class_feature_of S)
+      | add_classes S =
+        fold (`(Sorts.super_classes classes)
+              #> swap #> op ::
+              #> subtract (op =) @{sort type}
+              #> map class_feature_of
+              #> union (op = o pairself fst)) S
     fun do_add_type (Type (s, Ts)) =
         (not (member (op =) bad_types s)
          ? insert (op = o pairself fst) (type_feature_of s))