# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268056886 -3600
# Node ID 226693549aa0a8214655ff9606ed7a744452458f
# Parent  f00761b5957ed5b7d1f33e8819004305385992c6# Parent  e72d9d9eada309bf4a12eb73c586d2fb8bf7a465
merged

diff -r e72d9d9eada3 -r 226693549aa0 Nominal/Nominal2_Atoms.thy
--- a/Nominal/Nominal2_Atoms.thy	Mon Mar 08 14:31:04 2010 +0100
+++ b/Nominal/Nominal2_Atoms.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -140,12 +140,13 @@
 
 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)"
-
+*)
 
 subsection {* A lemma for proving instances of class @{text at}. *}
 
diff -r e72d9d9eada3 -r 226693549aa0 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 08 14:31:04 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -331,9 +331,9 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
-  val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
+  val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
   val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
-  val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))