diff -r 3d54fcc5f41a -r 6f3b75135638 Quot/Nominal/Perm.thy
--- a/Quot/Nominal/Perm.thy	Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Thu Feb 18 23:07:52 2010 +0100
@@ -55,7 +55,7 @@
     val lthy =
       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
     (* TODO: Use the version of prmrec that gives the names explicitely. *)
-    val (perm_ldef, lthy') =
+    val ((_, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
     val perm_frees =