--- a/Nominal/Nominal2.thy	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/Nominal2.thy	Thu Nov 03 13:19:23 2011 +0000
@@ -177,7 +177,7 @@
 
   val lthy1 = Named_Target.theory_init thy1
 
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) raw_full_dt_names' 
+  val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' 
   val {descr, sorts, ...} = hd dtinfos
 
   val raw_tys = Datatype_Aux.get_rec_types descr sorts
@@ -194,7 +194,7 @@
   val raw_induct_thms = #inducts (hd dtinfos)
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
-  val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy1) (hd raw_full_dt_names')
+  val raw_size_thms = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names')
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop
 
@@ -493,7 +493,7 @@
   val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
 
   val (_, lthy9') = lthyC
-     |> Local_Theory.declaration false (K (fold register_info infos))
+     |> Local_Theory.declaration {syntax = false, pervasive = false} (K (fold register_info infos))
      |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
@@ -685,7 +685,7 @@
     map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs
 
   (* this theory is used just for parsing *)
-  val thy = ProofContext.theory_of lthy  
+  val thy = Proof_Context.theory_of lthy  
   val tmp_thy = Theory.copy thy 
 
   val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') =