diff -r e5413596e098 -r bd40c5cb803d Quot/Nominal/Perm.thy
--- a/Quot/Nominal/Perm.thy	Thu Feb 18 11:19:16 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Thu Feb 18 11:28:20 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 =