src/HOL/Bali/WellForm.thy
changeset 52037 837211662fb8
parent 51717 9e7d1c139569
child 55518 1ddb2edf5ceb
     1.1 --- a/src/HOL/Bali/WellForm.thy	Thu May 16 15:21:12 2013 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Thu May 16 17:39:38 2013 +0200
     1.3 @@ -2258,7 +2258,7 @@
     1.4  qed
     1.5  declare split_paired_All [simp] split_paired_Ex [simp]
     1.6  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
     1.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     1.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     1.9  
    1.10  (* Tactical version *)
    1.11  (*
    1.12 @@ -2427,7 +2427,7 @@
    1.13  done
    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 -setup {* map_theory_simpset (fn ctxt => ctxt 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  lemma ty_expr_is_type: 
    1.20  "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"