diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Sat Jul 21 23:25:00 2007 +0200
@@ -373,7 +373,7 @@
 apply (auto simp add: appl_methds_foo_Base)
 done
 
-ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
+ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
 lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
   Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
 apply (tactic t) -- ";;"
@@ -399,7 +399,7 @@
 apply (rule max_spec_foo_Base)
 done
 
-ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
+ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *}
 
 declare split_if [split del]
 declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]