Fix to get old alpha.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 09 Mar 2010 17:02:29 +0100
changeset 1377 34317cb033f2
parent 1376 56efa1e854bf
child 1378 5c6c950812b1
Fix to get old alpha.
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
 *}