diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Mon Aug 16 17:39:16 2010 +0800
@@ -14,10 +14,10 @@
     Quotient_Info.qconsts_info list * local_theory
 
   val define_qperms: typ list -> string list -> (string * term * mixfix) list -> 
-    thm list -> theory -> theory
+    thm list -> local_theory -> local_theory
 
   val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
-    theory -> theory
+    local_theory -> local_theory
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -45,34 +45,38 @@
 
 
 (* defines the quotient permutations and proves pt-class *)
-fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy =
+fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy =
 let
-  val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy
+  val lthy' = 
+    lthy
+    |> Local_Theory.exit_global
+    |> Class.instantiation (qfull_ty_names, [], @{sort pt}) 
   
-  val (_, lthy') = define_qconsts qtys perm_specs lthy
+  val (_, lthy'') = define_qconsts qtys perm_specs lthy'
 
-  val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws
+  val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy'') raw_perm_laws
 
   fun tac _ =
     Class.intro_classes_tac [] THEN
       (ALLGOALS (resolve_tac lifted_perm_laws))
 in
-  lthy'
+  lthy''
   |> Class.prove_instantiation_exit tac 
+  |> Named_Target.theory_init
 end
 
 
 (* defines the size functions and proves size-class *)
-fun define_qsizes qtys qfull_ty_names size_specs thy =
+fun define_qsizes qtys qfull_ty_names size_specs lthy =
 let
-  val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy
-  
-  val (_, lthy') = define_qconsts qtys size_specs lthy
-
   fun tac _ = Class.intro_classes_tac []
 in
-  lthy'
+  lthy
+  |> Local_Theory.exit_global
+  |> Class.instantiation (qfull_ty_names, [], @{sort size})
+  |> snd o (define_qconsts qtys size_specs)
   |> Class.prove_instantiation_exit tac
+  |> Named_Target.theory_init
 end
 
 end (* structure *)