--- a/src/HOL/Tools/hologic.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Mon Jun 28 15:03:07 2010 +0200
@@ -315,12 +315,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.prod_case", (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.split", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.prod_case", 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*)
@@ -427,7 +427,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ 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