--- a/src/Doc/Implementation/Isar.thy Thu Jun 19 12:01:26 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy Thu Jun 19 12:05:10 2014 +0200
@@ -471,7 +471,7 @@
notepad
begin
- fix a b c
+ fix a b c :: 'a
assume [my_simp]: "a \<equiv> b"
assume [my_simp]: "b \<equiv> c"
have "a \<equiv> c" by my_simp'