src/HOL/Bali/TypeSafe.thy
changeset 52037 837211662fb8
parent 51717 9e7d1c139569
child 54859 64ff7f16d5b7
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu May 16 15:21:12 2013 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu May 16 17:39:38 2013 +0200
     1.3 @@ -756,7 +756,7 @@
     1.4  declare split_if     [split] split_if_asm     [split] 
     1.5          option.split [split] option.split_asm [split]
     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  
    1.11  lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
    1.12 @@ -925,7 +925,7 @@
    1.13  declare split_if     [split] split_if_asm     [split] 
    1.14          option.split [split] option.split_asm [split]
    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  
    1.20  subsection "accessibility"