diff -r 9229d09363c0 -r 4ff1dc2aa18d src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:54 2007 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:55 2007 +0200
@@ -182,10 +182,8 @@
 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
 *}
-ML{*
-Unify.search_bound := 40;
-Unify.trace_bound  := 40
-*}
+
+declare [[unify_search_bound = 40, unify_trace_bound = 40]]
 
 
 theorem eval_evals_exec_type_sound: 
@@ -369,10 +367,8 @@
 apply (simp (no_asm_simp))+ 
 
 done
-ML{*
-Unify.search_bound := 20;
-Unify.trace_bound  := 20
-*}
+
+declare [[unify_search_bound = 20, unify_trace_bound = 20]]
 
 
 lemma eval_type_sound: "!!E s s'.