equal
deleted
inserted
replaced
101 (* exists such a pi; otherwise raises EQVT_FORM *) |
101 (* exists such a pi; otherwise raises EQVT_FORM *) |
102 fun get_pi t thy = |
102 fun get_pi t thy = |
103 let fun get_pi_aux s = |
103 let fun get_pi_aux s = |
104 (case s of |
104 (case s of |
105 (Const (@{const_name "perm"} ,typrm) $ |
105 (Const (@{const_name "perm"} ,typrm) $ |
106 (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $ |
106 (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $ |
107 (Var (n,ty))) => |
107 (Var (n,ty))) => |
108 let |
108 let |
109 (* FIXME: this should be an operation the library *) |
109 (* FIXME: this should be an operation the library *) |
110 val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm) |
110 val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm) |
111 in |
111 in |