--- a/Nominal/NewParser.thy	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal/NewParser.thy	Thu Aug 12 21:29:35 2010 +0800
@@ -341,7 +341,7 @@
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val lthy3 = Theory_Target.init NONE thy;
+  val lthy3 = Named_Target.init NONE thy;
 
   val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
@@ -577,7 +577,7 @@
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
   (* use Local_Theory.theory_result *)
   val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
-  val lthy13 = Theory_Target.init NONE thy';
+  val lthy13 = Named_Target.init NONE thy';
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
@@ -618,7 +618,7 @@
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val _ = warning "Instantiating FS";
-  val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
+  val lthy21 = Class.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
   val lthy22 = Class.prove_instantiation_instance tac lthy21
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos;