# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1305043822 -3600
# Node ID 2cb34b1e7e1961316a42ad5be87c425254125864
# Parent  542ff50555f515228851328b0d133c0bb2dde6f8
made the subtyping work again

diff -r 542ff50555f5 -r 2cb34b1e7e19 Nominal/Atoms.thy
--- a/Nominal/Atoms.thy	Tue May 10 07:47:06 2011 +0100
+++ b/Nominal/Atoms.thy	Tue May 10 17:10:22 2011 +0100
@@ -3,9 +3,9 @@
 
     Instantiations of concrete atoms 
 *)
+
 theory Atoms
 imports Nominal2_Base
-uses "~~/src/Tools/subtyping.ML"
 begin
 
 
@@ -225,12 +225,11 @@
 
 declare [[coercion "atom::var2\<Rightarrow>atom"]]
 
-(*
 lemma
   fixes a::"var1" and b::"var2"
   shows "a \<sharp> t \<and> b \<sharp> t"
 oops
-*)
+
 
 (* does not yet work: it needs image as
    coercion map *)