1.1 --- a/src/HOL/Library/simps_case_conv.ML	Tue Nov 12 13:47:24 2013 +0100
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Tue Nov 12 13:47:24 2013 +0100
     1.3 @@ -22,9 +22,9 @@
     1.4    | collect_Tcons (TFree _) = []
     1.5    | collect_Tcons (TVar _) = []
     1.6  
     1.7 -fun get_split_ths thy = collect_Tcons
     1.8 +fun get_split_ths ctxt = collect_Tcons
     1.9      #> distinct (op =)
    1.10 -    #> map_filter (Datatype_Data.get_info thy)
    1.11 +    #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
    1.12      #> map #split
    1.13  
    1.14  val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
    1.15 @@ -80,7 +80,7 @@
    1.16      val case_arg = HOLogic.mk_tuple (flat def_frees)
    1.17      val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
    1.18        case_arg (pattern ~~ rhss)
    1.19 -    val split_thms = get_split_ths (Proof_Context.theory_of ctxt') (fastype_of case_arg)
    1.20 +    val split_thms = get_split_ths ctxt' (fastype_of case_arg)
    1.21      val t = (list_comb (fun_t, def_pats), cases)
    1.22        |> HOLogic.mk_eq
    1.23        |> HOLogic.mk_Trueprop
    1.24 @@ -194,7 +194,7 @@
    1.25  fun to_simps ctxt thm =
    1.26    let
    1.27      val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
    1.28 -    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
    1.29 +    val splitthms = get_split_ths ctxt T
    1.30    in gen_to_simps ctxt splitthms thm end
    1.31  
    1.32