src/HOL/Tools/hologic.ML
changeset 37591 d3daea901123
parent 37389 09467cdfa198
child 37676 f433cb9caea4
     1.1 --- a/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -315,12 +315,12 @@
     1.4    end;
     1.5  
     1.6  fun split_const (A, B, C) =
     1.7 -  Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
     1.8 +  Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
     1.9  
    1.10  fun mk_split t =
    1.11    (case Term.fastype_of t of
    1.12      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
    1.13 -      Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
    1.14 +      Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
    1.15    | _ => raise TERM ("mk_split: bad body type", [t]));
    1.16  
    1.17  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
    1.18 @@ -427,7 +427,7 @@
    1.19  val strip_psplits =
    1.20    let
    1.21      fun strip [] qs Ts t = (t, rev Ts, qs)
    1.22 -      | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
    1.23 +      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
    1.24            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
    1.25        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
    1.26        | strip (p :: ps) qs Ts t = strip ps qs