src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 36037 b1b21a8f6362
parent 36035 d82682936c52
child 36038 385f706eff24
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:53 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:54 2010 +0200
     1.3 @@ -1940,7 +1940,8 @@
     1.4          (case alternative_function_of (ProofContext.theory_of ctxt) name mode of
     1.5            SOME alt_function_name =>
     1.6              let
     1.7 -              val (inpTs, outpTs) = split_modeT' mode (binder_types T)
     1.8 +              val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
     1.9 +                mode (binder_types T)
    1.10                val bs = map (pair "x") inpTs
    1.11                val bounds = map Bound (rev (0 upto (length bs) - 1))
    1.12                val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs)