src/HOL/Bali/WellForm.thy

       by (cases emh type: prod) (auto dest: accmethd_SomeD)
   qed
 qed
 declare split_paired_All [simp] split_paired_Ex [simp]
 setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
 
 (* Tactical version *)
 (*
 lemma dynamic_mheadsD: "  
  \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y;  

              simp add: is_acc_type_def
     )
 done
 declare split_paired_All [simp] split_paired_Ex [simp]
 setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
 
 lemma ty_expr_is_type: 
 "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
 by (auto dest!: wt_is_type)
 lemma ty_var_is_type: