--- a/Nominal/nominal_dt_quot.ML	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sat Aug 14 23:33:23 2010 +0800
@@ -42,18 +42,21 @@
 
 
 (* defines the quotient permutations *)
-fun qperm_defs qtys full_tnames name_term_pairs thms thy =
+fun qperm_defs qtys full_tnames perm_specs thms thy =
 let
   val lthy =
     Class.instantiation (full_tnames, [], @{sort pt}) thy;
-  val (_, lthy') = qconst_defs qtys name_term_pairs lthy;
+  
+  val (_, lthy') = qconst_defs qtys perm_specs lthy;
+
   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
+
   fun tac _ =
     Class.intro_classes_tac [] THEN
-    (ALLGOALS (resolve_tac lifted_thms))
-  val lthy'' = Class.prove_instantiation_instance tac lthy'
+      (ALLGOALS (resolve_tac lifted_thms))
 in
-  Local_Theory.exit_global lthy''
+  lthy'
+  |> Class.prove_instantiation_exit tac 
 end