# HG changeset patch
# User wenzelm
# Date 966682036 -7200
# Node ID 8b3ab0244560c37d7f827dd70571cee6efd25d2c
# Parent  80d14ea0e20057f655176b9e639cbe2cb7f3de02
fixed text;

diff -r 80d14ea0e200 -r 8b3ab0244560 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Sat Aug 19 12:45:11 2000 +0200
+++ b/src/HOL/Lambda/Type.thy	Sat Aug 19 12:47:16 2000 +0200
@@ -353,7 +353,7 @@
     txt {* @{term Var} *}
     apply (intro strip)
     apply (case_tac "n = i")
-     txt {* #{term "n = i"} *}
+     txt {* @{term "n = i"} *}
      apply (case_tac rs)
       apply simp
      apply simp