1.1 --- a/src/HOL/Bali/WellForm.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -2127,7 +2127,7 @@
     1.4  qed
     1.5  
     1.6  declare split_paired_All [simp del] split_paired_Ex [simp del]
     1.7 -declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     1.8 +setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
     1.9  setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    1.10  
    1.11  lemma dynamic_mheadsD:   
    1.12 @@ -2258,7 +2258,7 @@
    1.13  qed
    1.14  declare split_paired_All [simp] split_paired_Ex [simp]
    1.15  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.16 -declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.17 +setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
    1.18  
    1.19  (* Tactical version *)
    1.20  (*
    1.21 @@ -2401,7 +2401,7 @@
    1.22    
    1.23  
    1.24  declare split_paired_All [simp del] split_paired_Ex [simp del]
    1.25 -declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    1.26 +setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
    1.27  setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    1.28  
    1.29  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
    1.30 @@ -2427,7 +2427,7 @@
    1.31  done
    1.32  declare split_paired_All [simp] split_paired_Ex [simp]
    1.33  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.34 -declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.35 +setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
    1.36  
    1.37  lemma ty_expr_is_type: 
    1.38  "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"