diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/NewParser.thy	Mon Aug 16 17:39:16 2010 +0800
@@ -331,12 +331,10 @@
   
   (* definitions of raw permutations *)
   val _ = warning "Definition of raw permutations";
-  val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
+  val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
     if get_STEPS lthy0 > 1 
-    then Local_Theory.theory_result 
-      (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0
+    then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0
     else raise TEST lthy0
-  val lthy2a = Named_Target.reinit lthy2 lthy2
  
   (* noting the raw permutations as eqvt theorems *)
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
@@ -511,18 +509,14 @@
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
     if get_STEPS lthy > 18
-    then Local_Theory.theory 
-      (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8 
+    then define_qperms qtys qty_full_names qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
-  val lthy9' = 
+  val lthy9a = 
     if get_STEPS lthy > 19
-    then Local_Theory.theory 
-      (define_qsizes qtys qty_full_names qsize_descr) lthy9
+    then define_qsizes qtys qty_full_names qsize_descr lthy9
     else raise TEST lthy9
 
-  val lthy9a = Named_Target.reinit lthy9' lthy9'
-
   val qconstrs = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
@@ -602,12 +596,9 @@
   val qalphabn_defs = map #def qalpha_info
   
   val _ = warning "Lifting permutations";
-  val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
-  (* use Local_Theory.theory_result *)
-  val thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy;
-  val lthy13 = Named_Target.init "" thy';
+  val lthy13 = define_qperms qtys qty_full_names dd raw_perm_laws lthy12c
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);