# HG changeset patch # User Cezary Kaliszyk # Date 1266414272 -3600 # Node ID f6e9ae54b85522b2bf3b31b427bf7c9173832eda # Parent 9cb99a28b40ee5db8aab06e9108dfe8078bc4de0 Now should work. diff -r 9cb99a28b40e -r f6e9ae54b855 Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Wed Feb 17 14:35:06 2010 +0100 +++ b/Quot/Nominal/Fv.thy Wed Feb 17 14:44:32 2010 +0100 @@ -39,8 +39,6 @@ [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] *) -ML foldr1 -ML fold ML {* val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; val sorts = []; @@ -51,6 +49,7 @@ "fv_" ^ name_of_typ (nth_dtyp i)) descr); val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; val fv_frees = map Free (fv_names ~~ fv_types); + fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] fun mk_union sets = fold (fn a => fn b => if a = noatoms then b else @@ -58,7 +57,7 @@ HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms; fun mk_diff a b = if b = noatoms then a else - HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (a, b); + HOLogic.mk_binop @{const_name minus} (a, b); fun fv_eq_constr i (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; @@ -66,12 +65,14 @@ val args = map Free (names ~~ Ts); val c = Const (cname, Ts ---> (nth_dtyp i)); val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); - fun fv_bind (_, i) = @{term "{} :: atom set"} + (* TODO we assume that all can be 'atomized' *) + fun fv_bind (NONE, i) = mk_single_atom (nth args i) + | fv_bind (SOME f, i) = f $ (nth args i); fun fv_arg ((dt, x), bindxs) = let val arg = if is_rec_type dt then nth fv_frees (body_index dt) $ x - (* TODO: we just assume everything is a 'name' *) + (* TODO: we just assume everything can be 'atomized' *) else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] val sub = mk_union (map fv_bind bindxs) in