--- a/Nominal/nominal_dt_quot.ML	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Thu Aug 12 21:29:35 2010 +0800
@@ -45,7 +45,7 @@
 fun qperm_defs qtys full_tnames name_term_pairs thms thy =
 let
   val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+    Class.instantiation (full_tnames, [], @{sort pt}) thy;
   val (_, lthy') = qconst_defs qtys name_term_pairs lthy;
   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
   fun tac _ =