src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 45879 71b8d0d170b1
parent 45822 843dc212f69e
child 45906 0aaeb5520f2f
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 20:36:17 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 21:54:32 2011 +0100
     1.3 @@ -903,9 +903,9 @@
     1.4  fun datatype_names_of_case_name thy case_name =
     1.5    map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
     1.6  
     1.7 -fun make_case_distribs new_type_names descr thy =
     1.8 +fun make_case_distribs case_names descr thy =
     1.9    let
    1.10 -    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
    1.11 +    val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
    1.12      fun make comb =
    1.13        let
    1.14          val Type ("fun", [T, T']) = fastype_of comb;
    1.15 @@ -932,10 +932,10 @@
    1.16  
    1.17  fun case_rewrites thy Tcon =
    1.18    let
    1.19 -    val {descr, ...} = Datatype.the_info thy Tcon
    1.20 +    val {descr, case_name, ...} = Datatype.the_info thy Tcon
    1.21    in
    1.22      map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
    1.23 -      (make_case_distribs [Tcon] [descr] thy)
    1.24 +      (make_case_distribs [case_name] [descr] thy)
    1.25    end
    1.26  
    1.27  fun instantiated_case_rewrites thy Tcon =