# HG changeset patch
# User blanchet
# Date 1386560699 -3600
# Node ID fed04f257898800238d2e4ff054897a57a10dea3
# Parent  b08e1bbde10a967379b87ea09e71345a23611380
disable generalization in MaSh until it is shown to help

diff -r b08e1bbde10a -r fed04f257898 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 09 04:03:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 09 04:44:59 2013 +0100
@@ -616,6 +616,8 @@
     cls_of [] (Graph.maximals graph)
   end
 
+val generalize_goal = false
+
 fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -670,11 +672,13 @@
           []
         else
           let
-            fun strs_of_sort S =
-              S |> (if in_goal then Sorts.complete_sort alg else single o hd)
-                |> map massage_long_name
+            val strs_of_sort =
+              (if generalize_goal andalso in_goal then Sorts.complete_sort alg
+               else single o hd)
+              #> map massage_long_name
             fun strs_of_type_arg (T as Type (s, _)) =
-                massage_long_name s :: (if in_goal then strs_of_sort (sort_of_type alg T) else [])
+                massage_long_name s ::
+                (if generalize_goal andalso in_goal then strs_of_sort (sort_of_type alg T) else [])
               | strs_of_type_arg (TFree (s, S)) = strs_of_sort S
               | strs_of_type_arg (TVar (s, S)) = strs_of_sort S