src/HOL/Product_Type.thy
changeset 26480 544cef16045b
parent 26358 d6a508c16908
child 26588 d83271bfaba5
     1.1 --- a/src/HOL/Product_Type.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4    this rule directly --- it loops!
     1.5  *}
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9    val unit_eq_proc =
    1.10      let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
    1.11        Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
    1.12 @@ -323,7 +323,7 @@
    1.13  
    1.14  lemmas split_tupled_all = split_paired_all unit_all_eq2
    1.15  
    1.16 -ML_setup {*
    1.17 +ML {*
    1.18    (* replace parameters of product type by individual component parameters *)
    1.19    val safe_full_simp_tac = generic_simp_tac true (true, false, false);
    1.20    local (* filtering with exists_paired_all is an essential optimization *)
    1.21 @@ -429,7 +429,7 @@
    1.22    split_beta}.
    1.23  *}
    1.24  
    1.25 -ML_setup {*
    1.26 +ML {*
    1.27  
    1.28  local
    1.29    val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]