# HG changeset patch
# User wenzelm
# Date 1403172310 -7200
# Node ID 1dc320dc2ada1a30b07b6ce2c47278f53706a7a5
# Parent  d6393137b161e9dc3173dee432a63cf54b43a22f
tuned;

diff -r d6393137b161 -r 1dc320dc2ada src/Doc/Implementation/Isar.thy
--- 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'