# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272535904 -7200
# Node ID 92f40c13d5814a024d8fd5aea21c6c43caffa527
# Parent  4538d63ecc9b6115652d5c3be303facf8903844e
revert 0c9ef14e9ba4

diff -r 4538d63ecc9b -r 92f40c13d581 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu Apr 29 11:54:39 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 12:11:44 2010 +0200
@@ -50,7 +50,7 @@
   val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
   val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 in
-  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t)
+  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
 end;
 
 fun mk_diff a b =
@@ -209,7 +209,7 @@
 *}
 
 ML {*
-fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses lthy =
+fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr as dt_descr, sorts, ...} = dt_info;
@@ -219,12 +219,12 @@
   val fv_frees = map Free (fv_names ~~ fv_types);
 
   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
-    fv_bns thy dt_descr sorts fv_frees bn_funs bclauses;
+    fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
   val fvbns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
 
-  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
+  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums);
 
   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)