# HG changeset patch
# User blanchet
# Date 1384260444 -3600
# Node ID f6950854855d3675566f7c4ebb7caff11287044f
# Parent  418a183fbe2176241b7cf46c67d5f449dc2bd9d7
ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

diff -r 418a183fbe21 -r f6950854855d src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Tue Nov 12 13:47:24 2013 +0100
@@ -22,9 +22,9 @@
   | collect_Tcons (TFree _) = []
   | collect_Tcons (TVar _) = []
 
-fun get_split_ths thy = collect_Tcons
+fun get_split_ths ctxt = collect_Tcons
     #> distinct (op =)
-    #> map_filter (Datatype_Data.get_info thy)
+    #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
     #> map #split
 
 val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
@@ -80,7 +80,7 @@
     val case_arg = HOLogic.mk_tuple (flat def_frees)
     val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
       case_arg (pattern ~~ rhss)
-    val split_thms = get_split_ths (Proof_Context.theory_of ctxt') (fastype_of case_arg)
+    val split_thms = get_split_ths ctxt' (fastype_of case_arg)
     val t = (list_comb (fun_t, def_pats), cases)
       |> HOLogic.mk_eq
       |> HOLogic.mk_Trueprop
@@ -194,7 +194,7 @@
 fun to_simps ctxt thm =
   let
     val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
-    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
+    val splitthms = get_split_ths ctxt T
   in gen_to_simps ctxt splitthms thm end