# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272401150 -7200
# Node ID 0c9ef14e9ba4e4efd71569c80c79a29e2ccb8cf2
# Parent  84a13d1e251111980a865c6b07bbdcd7a5a84fc1
some tuning

diff -r 84a13d1e2511 -r 0c9ef14e9ba4 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Apr 27 22:45:50 2010 +0200
@@ -34,11 +34,9 @@
 fun mk_plus p q =
  @{term "plus::perm => perm => perm"} $ p $ q
 
-fun perm_ty ty = @{typ perm} --> ty --> ty 
-
+fun perm_ty ty = @{typ "perm"} --> ty --> ty 
 fun mk_perm_ty ty p trm =
   Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
-
 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
@@ -47,7 +45,8 @@
 
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
-fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t;
+fun atom_ty ty = ty --> @{typ "atom"}
+fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
 fun mk_equiv r = r RS @{thm eq_reflection};
diff -r 84a13d1e2511 -r 0c9ef14e9ba4 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal/NewFv.thy	Tue Apr 27 22:45:50 2010 +0200
@@ -15,6 +15,7 @@
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 
   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
+
   val noatoms = @{term "{} :: atom set"};
   fun mk_union sets =
     fold (fn a => fn b =>
@@ -25,8 +26,8 @@
 *}
 
 ML {*
-fun is_atom thy typ =
-  Sign.of_sort thy (typ, @{sort at})
+fun is_atom thy ty =
+  Sign.of_sort thy (ty, @{sort at})
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
   | is_atom_set _ _ = false;
@@ -40,7 +41,7 @@
   val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
   val img_ty = atom_ty --> ty --> @{typ "atom set"};
 in
-  (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+  (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)
 end;
 
 fun mk_atom_fset t =
@@ -50,7 +51,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) $ Const (@{const_name atom}, atom_ty) $ t))
+  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t)
 end;
 
 fun mk_diff a b =
@@ -60,21 +61,25 @@
 *}
 
 ML {*
-fun atoms thy x =
+fun atoms thy t =
 let
-  val ty = fastype_of x;
+  val ty = fastype_of t;
 in
-  if is_atom thy ty then mk_single_atom x else
-  if is_atom_set thy ty then mk_atom_set x else
-  if is_atom_fset thy ty then mk_atom_fset x else
-  @{term "{} :: atom set"}
+  if is_atom thy ty 
+    then mk_single_atom t 
+  else if is_atom_set thy ty 
+    then mk_atom_set t 
+  else if is_atom_fset thy ty 
+    then mk_atom_fset t 
+  else noatoms
 end
 *}
 
 ML {*
 fun setify x =
-  if fastype_of x = @{typ "atom list"} then
-  Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
+  if fastype_of x = @{typ "atom list"} 
+    then @{term "set::atom list \<Rightarrow> atom set"} $ x 
+    else x
 *}
 
 ML {*
@@ -199,6 +204,7 @@
   map2 fv_constr constrs bmll
 end
 *}
+
 ML {*
 val by_pat_completeness_auto =
   Proof.global_terminal_proof
@@ -213,7 +219,7 @@
 
 
 ML {*
-fun define_fv dt_info bns bmlll lthy =
+fun define_raw_fv dt_info bns bmlll lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr, sorts, ...} = dt_info;
diff -r 84a13d1e2511 -r 0c9ef14e9ba4 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 22:45:50 2010 +0200
@@ -277,7 +277,7 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end