# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269818604 -7200
# Node ID 8c0eef2b84e7241065947685d935230f62ac3b28
# Parent  0b2535a72fd070ef1c71a97869a51bd9420467ab
fixed a problem due to a change in type-def (needs new Isabelle)

diff -r 0b2535a72fd0 -r 8c0eef2b84e7 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Mon Mar 29 00:30:47 2010 +0200
+++ b/Nominal/nominal_atoms.ML	Mon Mar 29 01:23:24 2010 +0200
@@ -43,11 +43,11 @@
     (* typedef *)
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
-    val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
+    val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
       Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
-    val newT = #abs_type info;
+    val newT = #abs_type (fst info);
     val RepC = Const (Rep_name, newT --> atomT);
     val AbsC = Const (Abs_name, atomT --> newT);
     val a = Free ("a", newT);