--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Feb 02 13:26:38 2000 +0100
@@ -120,7 +120,7 @@
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
by (exhaust_tac "v" 1);
-by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null]))));
+by (ALLGOALS (fast_tac (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
qed "Cast_conf2";
Goal
@@ -283,31 +283,31 @@
by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1
addsplits [option.split]) 1);
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
bd approx_stk_append_lemma 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
bd conf_RefTD 1;
by (Clarify_tac 1);
by(rename_tac "oloc oT ofs T'" 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
bd subtype_widen_methd 1;
ba 1;
ba 1;
be exE 1;
by(rename_tac "oT'" 1);
by (Clarify_tac 1);
-by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
+by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2);
ba 2;
by(Blast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by(forward_tac [method_in_md] 1);
ba 1;
back();
back();
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
ba 1;
back();