--- a/Nominal/nominal_dt_quot.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_dt_quot.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -9,10 +9,10 @@
 signature NOMINAL_DT_QUOT =
 sig
   val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
-    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory
+    thm list -> local_theory -> Quotient_Info.quotients list * local_theory
 
   val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
-    Quotient_Info.qconsts_info list * local_theory
+    Quotient_Info.quotconsts list * local_theory
 
   val define_qperms: typ list -> string list -> (string * sort) list -> 
     (string * term * mixfix) list -> thm list -> local_theory -> local_theory
@@ -69,9 +69,9 @@
   let
     val (qconst_infos, lthy') = 
       fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
-    val phi = ProofContext.export_morphism lthy' lthy
+    val phi = Proof_Context.export_morphism lthy' lthy
   in
-    (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
+    (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
   end
 
 
@@ -85,7 +85,7 @@
   
     val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
 
-    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
+    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws (Local_Theory.target_of lthy2)
 
     val lifted_perm_laws = 
       map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
@@ -185,7 +185,7 @@
   in
     Goal.prove ctxt' [] [] goal
       (K (HEADGOAL (supports_tac ctxt perm_simps)))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
   end
 
 fun prove_supports ctxt perm_simps qtrms =
@@ -210,7 +210,7 @@
   in
     Goal.prove ctxt' [] [] goals
       (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm
     |> map zero_var_indexes
   end
@@ -354,7 +354,7 @@
     val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
   in
     induct_prove qtys props qinduct (K ss_tac) ctxt'
-    |> ProofContext.export ctxt' ctxt
+    |> Proof_Context.export ctxt' ctxt
     |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
   end
 
@@ -380,7 +380,7 @@
               TRY o asm_full_simp_tac HOL_basic_ss]
   in
     induct_prove qtys props qinduct (K ss_tac) ctxt'
-    |> ProofContext.export ctxt' ctxt 
+    |> Proof_Context.export ctxt' ctxt 
     |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
   end
 
@@ -578,7 +578,7 @@
             (* proves goal "P" *)
             val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
               (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
-              |> singleton (ProofContext.export ctxt'' ctxt)  
+              |> singleton (Proof_Context.export ctxt'' ctxt)  
           in
             rtac side_thm 1 
           end) ctxt
@@ -612,7 +612,7 @@
       Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
   in
     map4 prove premss bclausesss exhausts' main_concls
-    |> ProofContext.export lthy'' lthy
+    |> Proof_Context.export lthy'' lthy
   end
 
 
@@ -697,7 +697,7 @@
     fun pat_tac ctxt thm =
       Subgoal.FOCUS (fn {params, context, ...} => 
         let
-          val thy = ProofContext.theory_of context
+          val thy = Proof_Context.theory_of context
           val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
           val vs = Term.add_vars (prop_of thm) []
           val vs_tys = map (Type.legacy_freeze_type o snd) vs
@@ -719,7 +719,7 @@
         THEN RANGE (map (pat_tac context) exhausts) 1
         THEN prove_termination_ind context 1
         THEN ALLGOALS size_simp_tac)
-    |> ProofContext.export lthy'' lthy
+    |> Proof_Context.export lthy'' lthy
   end