# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266488900 -3600
# Node ID bd40c5cb803d84b4d379dc2a8811568f719e51b5
# Parent  e5413596e0988ba2511fb5972ab9d8eaa7c2c62f
Fix for new Isabelle (primrec)

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 =