--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:44 2010 +0200
@@ -103,7 +103,7 @@
let fun get_pi_aux s =
(case s of
(Const (@{const_name "perm"} ,typrm) $
- (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
+ (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)