src/HOL/IMP/Examples.ML

--- a/src/HOL/IMP/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -34,7 +34,7 @@
 val step = resolve_tac evalc.intrs 1;
 val simp = Asm_simp_tac 1;
 Goalw [factorial_def] "a~=b ==> \
-\ <factorial a b, Mem(a:=# 3)>  -c-> Mem(b:=# 6,a:=Numeral0)";
+\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6,a:=Numeral0)";
 by (ftac not_sym 1);
 by step;
 by  step;