# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268150549 -3600
# Node ID 34317cb033f23c64308eea76384df146915988bc
# Parent  56efa1e854bfdd2666b9cf81cbd7344ecdb07de5
Fix to get old alpha.

diff -r 56efa1e854bf -r 34317cb033f2 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 09 16:57:51 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 17:02:29 2010 +0100
@@ -328,7 +328,7 @@
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
      (add_binds alpha_eqs) [] lthy'')
 in
-  ((fvs, alphas), lthy'')
+  ((fvs, alphas), lthy''')
 end
 *}