src/HOL/MicroJava/J/JTypeSafe.thy

 ML{*
 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
 *}
 
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
 
 theorem eval_evals_exec_type_sound: 
 "wf_java_prog G ==>  
   (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->  
       (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  

 apply blast
 apply (simp (no_asm_simp))+ 
 
 done
 
-declare [[unify_search_bound = 20, unify_trace_bound = 20]]
-
 
 lemma eval_type_sound: "!!E s s'.  
   [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]  
   ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'"
 apply (simp (no_asm_simp) only: split_tupled_all)