merged

--- a/src/Doc/Nitpick/document/root.tex	Mon Aug 19 20:47:09 2013 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Tue Aug 20 04:59:54 2013 +0200
@@ -2,7 +2,7 @@
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage[english,french]{babel}
+\usepackage[english]{babel}
 \usepackage{color}
 \usepackage{footmisc}
 \usepackage{graphicx}
@@ -46,8 +46,6 @@
 %\renewcommand\labelitemi{$\bullet$}
 \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
 
-\selectlanguage{english}
-
 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
 Picking Nits \\[\smallskipamount]
 \Large A User's Guide to Nitpick for Isabelle/HOL}

--- a/src/Doc/Sledgehammer/document/root.tex	Mon Aug 19 20:47:09 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Aug 20 04:59:54 2013 +0200
@@ -2,7 +2,7 @@
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage[english,french]{babel}
+\usepackage[english]{babel}
 \usepackage{color}
 \usepackage{footmisc}
 \usepackage{graphicx}
@@ -48,8 +48,6 @@
 %\renewcommand\labelitemi{$\bullet$}
 \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
 
-\selectlanguage{english}
-
 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
 Hammering Away \\[\smallskipamount]
 \Large A User's Guide to Sledgehammer for Isabelle/HOL}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 20:47:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 04:59:54 2013 +0200
@@ -566,7 +566,8 @@
 val pat_tvar_prefix = "_"
 val pat_var_prefix = "_"
 
-val massage_long_name = Long_Name.base_name
+(* try "Long_Name.base_name" for shorter names *)
+fun massage_long_name s = s
 
 val crude_str_of_sort =
   space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
@@ -626,10 +627,11 @@
       | pattify_term _ args _ (Const (x as (s, _))) =
         if fst (is_built_in x args) then [] else [massage_long_name s]
       | pattify_term _ _ _ (Free (s, T)) =
-        if member (op =) fixes s then
-          [massage_long_name (thy_name ^ Long_Name.separator ^ s)]
-        else
-          [pat_var_prefix ^ crude_str_of_typ T]
+        [pat_var_prefix ^ crude_str_of_typ T]
+        |> (if member (op =) fixes s then
+              cons (massage_long_name (thy_name ^ Long_Name.separator ^ s))
+            else
+              I)
       | pattify_term _ _ _ (Var (_, T)) = [pat_var_prefix ^ crude_str_of_typ T]
       | pattify_term Ts _ _ (Bound j) =
         [pat_var_prefix ^ crude_str_of_typ (nth Ts j)]