# HG changeset patch
# User blanchet
# Date 1376967594 -7200
# Node ID 7e89edba3db64dad93dadac77a9e64d45ffcfe49
# Parent  d2afb0eb82e20434534c02a5134fc43f2d035516# Parent  6cd0feb85e35d0133b7392969ba3851c7fe13682
merged

diff -r 6cd0feb85e35 -r 7e89edba3db6 src/Doc/Nitpick/document/root.tex
--- 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}
diff -r 6cd0feb85e35 -r 7e89edba3db6 src/Doc/Sledgehammer/document/root.tex
--- 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}
diff -r 6cd0feb85e35 -r 7e89edba3db6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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)]