# HG changeset patch # User Cezary Kaliszyk # Date 1277276505 -7200 # Node ID 10f699b48ba580656bf9b21c75f82527d68b0302 # Parent bcb037806e16485c4b3360314f91c84dc2f3ba60 Un-do the second change to SingleLet. diff -r bcb037806e16 -r 10f699b48ba5 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Jun 23 08:49:33 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed Jun 23 09:01:45 2010 +0200 @@ -4,8 +4,6 @@ atom_decl name -ML {* val _ = cheat_equivp := true *} - nominal_datatype trm = Var "name" | App "trm" "trm"