src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 45701 615da8b8d758
parent 45461 130c90bb80b4
child 45822 843dc212f69e
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 30 21:14:01 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 30 23:30:08 2011 +0100
     1.3 @@ -932,13 +932,10 @@
     1.4  
     1.5  fun case_rewrites thy Tcon =
     1.6    let
     1.7 -    val info = Datatype.the_info thy Tcon
     1.8 -    val descr = #descr info
     1.9 -    val sorts = #sorts info
    1.10 -    val typ_names = the_default [Tcon] (#alt_names info)
    1.11 +    val {descr, sorts, ...} = Datatype.the_info thy Tcon
    1.12    in
    1.13      map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
    1.14 -      (make_case_distribs typ_names [descr] sorts thy)
    1.15 +      (make_case_distribs [Tcon] [descr] sorts thy)
    1.16    end
    1.17  
    1.18  fun instantiated_case_rewrites thy Tcon =