src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 44241 7943b69f0188
parent 43326 47cf4bc789aa
child 45450 dc2236b19a3d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -914,7 +914,7 @@
     1.4              val Ts = binder_types (fastype_of f')
     1.5              val bs = map Bound ((length Ts - 1) downto 0)
     1.6            in
     1.7 -            fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
     1.8 +            fold_rev absdummy Ts (f $ (list_comb (f', bs)))
     1.9            end
    1.10          val fs' = map apply_f fs
    1.11          val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
    1.12 @@ -949,7 +949,7 @@
    1.13        val T' = TFree (tname', HOLogic.typeS)
    1.14        val U = TFree (uname, HOLogic.typeS)
    1.15        val y = Free (yname, U)
    1.16 -      val f' = absdummy (U --> T', Bound 0 $ y)
    1.17 +      val f' = absdummy (U --> T') (Bound 0 $ y)
    1.18        val th' = Thm.certify_instantiate
    1.19          ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    1.20           [((fst (dest_Var f), (U --> T') --> T'), f')]) th