handling function types more carefully than in e98a06145530
authorbulwahn
Mon Sep 13 16:44:19 2010 +0200 (2010-09-13)
changeset 39312968c33be5c96
parent 39311 2bd067f80b92
child 39313 41ce0b56d858
handling function types more carefully than in e98a06145530
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:19 2010 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4  
     1.5  fun ho_args_of_typ T ts =
     1.6    let
     1.7 -    fun ho_arg (Type("fun", [_,_])) (SOME t) = [t]
     1.8 +    fun ho_arg (T as Type("fun", [_,_])) (SOME t) = if body_type T = @{typ bool} then [t] else []
     1.9        | ho_arg (Type("fun", [_,_])) NONE = raise Fail "mode and term do not match"
    1.10        | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2]))
    1.11           (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
    1.12 @@ -289,7 +289,7 @@
    1.13  
    1.14  fun ho_argsT_of_typ Ts =
    1.15    let
    1.16 -    fun ho_arg (T as Type("fun", [_,_])) = [T]
    1.17 +    fun ho_arg (T as Type("fun", [_,_])) = if body_type T = @{typ bool} then [T] else []
    1.18        | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) =
    1.19            ho_arg T1 @ ho_arg T2
    1.20        | ho_arg _ = []