equal
deleted
inserted
replaced
113 (Const ("Nominal.perm",typrm) $ |
113 (Const ("Nominal.perm",typrm) $ |
114 (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ |
114 (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ |
115 (Var (n,ty))) => |
115 (Var (n,ty))) => |
116 let |
116 let |
117 (* FIXME: this should be an operation the library *) |
117 (* FIXME: this should be an operation the library *) |
118 val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) |
118 val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm) |
119 in |
119 in |
120 if (Sign.of_sort thy (ty,[class_name])) |
120 if (Sign.of_sort thy (ty,[class_name])) |
121 then [(pi,typi)] |
121 then [(pi,typi)] |
122 else raise |
122 else raise |
123 EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) |
123 EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) |