diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/Store.ML
--- a/src/HOL/MicroJava/JVM/Store.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -5,6 +5,6 @@
 *)
 
 Goalw [newref_def]
- "hp x = None \\<longrightarrow> hp (newref hp) = None";
+ "hp x = None --> hp (newref hp) = None";
 by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
 qed_spec_mp "newref_None";