src/HOL/UNITY/Comp/Alloc.thy

       @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
       @{thm o_apply}, @{thm Let_def}])
 *}
 
 method_setup record_auto = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+  Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
 *} ""
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   apply (unfold sysOfAlloc_def Let_def)
   apply (rule inj_onI)

         (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
 *}
 
 method_setup rename_client_map = {*
   Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
+    SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
 *} ""
 
 text{*Lifting @{text Client_Increasing} to @{term systemState}*}
 lemma rename_Client_Increasing: "i : I
       ==> rename sysOfClient (plam x: I. rename client_map Client) :