diff -r c3ff26204d2a -r d29a8a6f3138 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Apr 28 11:44:36 2011 +0800
+++ b/Nominal/Nominal2.thy	Thu Apr 28 11:51:01 2011 +0800
@@ -323,19 +323,19 @@
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs
+    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
+    map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns
 
   val qfvs_descr = 
     map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
+    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs  alpha_bn_trms
 
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -344,7 +344,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns
      
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) = 
@@ -646,7 +646,7 @@
 
   val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = 
     tmp_thy
-    |> Sign.add_types pre_typs
+    |> Sign.add_types_global pre_typs
     |> prepare_dts dt_strs 
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
     ||>> prepare_bclauses dt_strs