--- 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]}
--- 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";