--- a/Nominal/nominal_dt_rawperm.ML	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML	Thu Aug 12 21:29:35 2010 +0800
@@ -117,7 +117,7 @@
   val perm_eqs = maps perm_eq dt_descr;
 
   val lthy =
-    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
+    Class.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
   val ((perm_funs, perm_eq_thms), lthy') =
     Primrec.add_primrec
@@ -140,7 +140,7 @@
   lthy'
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
-  |> Class_Target.prove_instantiation_exit_result morphism tac 
+  |> Class.prove_instantiation_exit_result morphism tac 
        (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
 end