--- a/src/HOL/Nominal/nominal_permeq.ML Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Mar 05 12:08:00 2009 +0100
@@ -110,7 +110,7 @@
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
- val name = Sign.base_name n
+ val name = NameSpace.base_name n
val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
@@ -198,8 +198,8 @@
Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
- val tname' = Sign.base_name tname
- val uname' = Sign.base_name uname
+ val tname' = NameSpace.base_name tname
+ val uname' = NameSpace.base_name uname
in
if pi1 <> pi2 then (* only apply the composition rule in this case *)
if T = U then