# HG changeset patch
# User blanchet
# Date 1384199460 -3600
# Node ID 3514fdfdf59b0b0c6e461cf09649375aa8cb1b03
# Parent  27246f8b2dac6bd513c14d1007646eb6f8cdaa99
minor doc fix

diff -r 27246f8b2dac -r 3514fdfdf59b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Nov 11 18:37:56 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Nov 11 20:51:00 2013 +0100
@@ -732,7 +732,7 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{list.distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
+\item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
 @{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
 @{thm list.distinct(2)[THEN notE, elim!, no_vars]}
 
diff -r 27246f8b2dac -r 3514fdfdf59b src/HOL/BNF/Tools/ctr_sugar.ML
--- a/src/HOL/BNF/Tools/ctr_sugar.ML	Mon Nov 11 18:37:56 2013 +0100
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Mon Nov 11 20:51:00 2013 +0100
@@ -297,7 +297,7 @@
     fun qualify mandatory =
       Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
 
-    fun dest_TFree_or_TVar (TFree p) = p
+    fun dest_TFree_or_TVar (TFree sS) = sS
       | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
       | dest_TFree_or_TVar _ = error "Invalid type argument";