# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281619775 -28800
# Node ID f2f611daf48011c069875105d54bfee19e2a020d
# Parent  79e4938808017acf11a947d3aa74cb84e6c3bb84
updated to Isabelle 12th Aug

diff -r 79e493880801 -r f2f611daf480 Nominal-General/nominal_atoms.ML
--- a/Nominal-General/nominal_atoms.ML	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal-General/nominal_atoms.ML	Thu Aug 12 21:29:35 2010 +0800
@@ -53,7 +53,7 @@
 
     (* at class instance *)
     val lthy =
-      Theory_Target.instantiation ([full_tname], [], @{sort at}) thy;
+      Class.instantiation ([full_tname], [], @{sort at}) thy;
     val ((_, (_, permute_ldef)), lthy) =
       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
     val ((_, (_, atom_ldef)), lthy) =
diff -r 79e493880801 -r f2f611daf480 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal/NewParser.thy	Thu Aug 12 21:29:35 2010 +0800
@@ -341,7 +341,7 @@
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val lthy3 = Theory_Target.init NONE thy;
+  val lthy3 = Named_Target.init NONE thy;
 
   val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
@@ -577,7 +577,7 @@
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
   (* use Local_Theory.theory_result *)
   val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
-  val lthy13 = Theory_Target.init NONE thy';
+  val lthy13 = Named_Target.init NONE thy';
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
@@ -618,7 +618,7 @@
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val _ = warning "Instantiating FS";
-  val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
+  val lthy21 = Class.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
   val lthy22 = Class.prove_instantiation_instance tac lthy21
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos;
diff -r 79e493880801 -r f2f611daf480 Nominal/nominal_dt_quot.ML
--- 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 _ =
diff -r 79e493880801 -r f2f611daf480 Nominal/nominal_dt_rawperm.ML
--- 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