src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 45906 0aaeb5520f2f
parent 45879 71b8d0d170b1
child 46634 c6d2fc7095ac
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 16 22:07:03 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Dec 17 12:10:37 2011 +0100
     1.3 @@ -623,7 +623,7 @@
     1.4      |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
     1.5        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
     1.6  
     1.7 -fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
     1.8 +fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
     1.9    | find_split_thm thy _ = NONE
    1.10  
    1.11  (* lifting term operations to theorems *)
    1.12 @@ -901,7 +901,7 @@
    1.13  (*** this should be part of the datatype package ***)
    1.14  
    1.15  fun datatype_names_of_case_name thy case_name =
    1.16 -  map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
    1.17 +  map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name)))
    1.18  
    1.19  fun make_case_distribs case_names descr thy =
    1.20    let