raising an exception instead of guessing some reasonable behaviour for this function
authorbulwahn
Tue, 07 Sep 2010 11:51:53 +0200
changeset 39422f302ed18f42f
parent 39421 edaf5a6ffa99
child 39423 0e505a4e500c
raising an exception instead of guessing some reasonable behaviour for this function
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Sep 07 11:51:53 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -222,10 +222,11 @@
     1.4          fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
     1.5            (map all_modes_of_typ' S) [Bool]
     1.6        else
     1.7 -        [Input, Output]
     1.8 +        raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
     1.9      end
    1.10    | all_modes_of_typ @{typ bool} = [Bool]
    1.11 -  | all_modes_of_typ T = all_modes_of_typ' T
    1.12 +  | all_modes_of_typ T =
    1.13 +    raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
    1.14  
    1.15  fun all_smodes_of_typ (T as Type ("fun", _)) =
    1.16    let