--- a/src/HOL/Tools/hologic.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Sun Sep 06 22:14:51 2015 +0200
@@ -349,12 +349,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.uncurry", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.uncurry", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -470,7 +470,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.uncurry", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
| strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
| strip (p :: ps) qs Ts t = strip ps qs