# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1313397802 -7200
# Node ID 27aab7a105eb02be15339402ce7bda702e782abf
# Parent  847972b7b5ba3837f44940f7c8c9239cdbb6f39f
updated for new Isabelle (11. Aug.)

diff -r 847972b7b5ba -r 27aab7a105eb Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Sun Aug 14 08:52:03 2011 +0200
+++ b/Nominal/Nominal2_Base.thy	Mon Aug 15 10:43:22 2011 +0200
@@ -1015,7 +1015,7 @@
 
 instance 
 apply(default)
-unfolding Inf_fun_def
+unfolding Inf_fun_def INF_def
 apply(perm_simp)
 apply(rule refl)
 done 
diff -r 847972b7b5ba -r 27aab7a105eb Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Sun Aug 14 08:52:03 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Mon Aug 15 10:43:22 2011 +0200
@@ -391,7 +391,7 @@
       hd names
       |> the o Induct.lookup_inductP ctxt
       |> fst o Rule_Cases.get
-      |> map fst
+      |> map (fst o fst)
 
     val _ = (case duplicates (op = o pairself fst) avoids of
         [] => ()