# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269245785 -3600
# Node ID 1694f32b480ac81a6a412da14df16a359873bed7
# Parent  2facd6645599691e2dd937b030495b9ffec94b01
some tuning

diff -r 2facd6645599 -r 1694f32b480a Nominal/Nominal2_Atoms.thy
--- a/Nominal/Nominal2_Atoms.thy	Sun Mar 21 22:27:08 2010 +0100
+++ b/Nominal/Nominal2_Atoms.thy	Mon Mar 22 09:16:25 2010 +0100
@@ -23,8 +23,6 @@
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
 
-instance at < at_base ..
-
 lemma supp_at_base: 
   fixes a::"'a::at_base"
   shows "supp a = {atom a}"
@@ -146,13 +144,12 @@
 
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
-(*
 syntax
   "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
 
 translations
-  "_atom_constrain a t" => "atom (_constrain a t)"
-*)
+  "_atom_constrain a t" => "CONST atom (_constrain a t)"
+
 
 subsection {* A lemma for proving instances of class @{text at}. *}