# HG changeset patch
# User nipkow
# Date 1262469439 -3600
# Node ID 33d44b1520c0158203c4a266e200e271d0ec80eb
# Parent  aec597ef135c501eec3d563bbcfa9ddfaa044dd0
another legacy "asm_lr"

diff -r aec597ef135c -r 33d44b1520c0 src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Sat Jan 02 21:31:33 2010 +0100
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Sat Jan 02 22:57:19 2010 +0100
@@ -210,14 +210,14 @@
   let ?phi  = "map OK phi"
   let ?cert = "make_cert ?step ?phi (OK None)"
 
-  from wt obtain 
+  from wt have
     0:          "0 < length ins" and
     length:     "length ins = length ?phi" and
     ck_bounded: "check_bounded ins et" and
     ck_types:   "check_types G mxs ?mxr ?phi" and
     wt_start:   "wt_start G C pTs mxl phi" and
     app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
-    by (simp (asm_lr) add: wt_method_def2)
+    by (simp_all add: wt_method_def2)
   
   have "semilat (JVMType.sl G mxs ?mxr)" 
     by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf])