src/HOL/Nominal/nominal_permeq.ML

             | _ => true)
   in
     case redex of 
         (* case pi o (f x) == (pi o f) (pi o x)          *)
         (Const("Nominal.perm",
-          Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
+          Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
             (if (applicable_app f) then
               let
                 val name = Long_Name.base_name n
                 val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
                 val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")

 (* folding the definition                                              *)
 
 fun perm_compose_simproc' sg ss redex =
   (case redex of
      (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
-       [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
-         Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $ 
+       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
+         Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
           pi2 $ t)) =>
     let
       val tname' = Long_Name.base_name tname
       val uname' = Long_Name.base_name uname
     in