src/HOL/Nominal/nominal_permeq.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4            Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
     1.5              (if (applicable_app f) then
     1.6                let
     1.7 -                val name = NameSpace.base_name n
     1.8 +                val name = Long_Name.base_name n
     1.9                  val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
    1.10                  val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
    1.11                in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
    1.12 @@ -198,8 +198,8 @@
    1.13           Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
    1.14            pi2 $ t)) =>
    1.15      let
    1.16 -      val tname' = NameSpace.base_name tname
    1.17 -      val uname' = NameSpace.base_name uname
    1.18 +      val tname' = Long_Name.base_name tname
    1.19 +      val uname' = Long_Name.base_name uname
    1.20      in
    1.21        if pi1 <> pi2 then  (* only apply the composition rule in this case *)
    1.22          if T = U then