--- a/Nominal/Ex/LF.thy	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/Ex/LF.thy	Thu Nov 03 13:19:23 2011 +0000
@@ -55,9 +55,9 @@
     TC_ass "ident" "kind"
   | C_ass "ident" "ty"
 
-types Sig = "sig_ass list"
-types Ctx = "(name \<times> ty) list"
-types Subst = "(name \<times> trm) list"
+type_synonym Sig = "sig_ass list"
+type_synonym Ctx = "(name \<times> ty) list"
+type_synonym Subst = "(name \<times> trm) list"
 
 inductive
     sig_valid  :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60)

--- 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') = 

--- a/Nominal/ROOT.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/ROOT.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -4,8 +4,8 @@
    ["Atoms",
     "Eqvt",
     "Ex/Weakening",
-    (*"Ex/Classical",*)    
-    "Ex/Datatypes",
+    "Ex/Classical",
+    (*"Ex/Datatypes",*)
     "Ex/Ex1",
     "Ex/ExPS3",
     "Ex/Multi_Recs",
@@ -22,7 +22,7 @@
     "Ex/Shallow",
     "Ex/SystemFOmega",
     "Ex/TypeSchemes",
-    "Ex/TypeVarsTest",
+    (*"Ex/TypeVarsTest",*)
     "Ex/Foo1",
     "Ex/Foo2",
     "Ex/CoreHaskell",

--- a/Nominal/nominal_atoms.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_atoms.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -62,9 +62,9 @@
       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
     val ((_, (_, atom_ldef)), lthy) =
       Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
-    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
-    val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
-    val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
+    val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
+    val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef;
+    val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef;
     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
     val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
     val thy = lthy

--- a/Nominal/nominal_dt_alpha.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -257,7 +257,7 @@
     val alpha_raw_induct_loc = #raw_induct alpha_info;
     val alpha_intros_loc = #intrs alpha_info;
     val alpha_cases_loc = #elims alpha_info;
-    val phi = ProofContext.export_morphism lthy' lthy;
+    val phi = Proof_Context.export_morphism lthy' lthy;
     
     val all_alpha_trms = all_alpha_trms_loc
       |> map (Morphism.term phi) 
@@ -318,7 +318,7 @@
            (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
   in
     Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm
     |> map Datatype_Aux.split_conj_thm
     |> flat
@@ -364,7 +364,7 @@
          THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
   in
     Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm
     |> map (fn th => th RS mp) 
     |> map Datatype_Aux.split_conj_thm
@@ -830,7 +830,7 @@
   in
     alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct 
       (raw_prove_perm_bn_tac alpha_result simps) ctxt
-     |> ProofContext.export ctxt' ctxt
+     |> Proof_Context.export ctxt' ctxt
      |> map atomize
      |> map single
      |> map (curry (op OF) perm_bn_rsp)

--- 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
 
 

--- a/Nominal/nominal_dt_rawfuns.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -261,7 +261,7 @@
  
     val {fs, simps, inducts, ...} = info; 
 
-    val morphism = ProofContext.export_morphism lthy'' lthy
+    val morphism = Proof_Context.export_morphism lthy'' lthy
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
     
@@ -334,7 +334,7 @@
 
       val {fs, simps, ...} = info;
 
-      val morphism = ProofContext.export_morphism lthy'' lthy
+      val morphism = Proof_Context.export_morphism lthy'' lthy
       val simps_exp = map (Morphism.thm morphism) (the simps)
     in
       (fs, simps_exp, lthy'')
@@ -467,7 +467,7 @@
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   HEADGOAL
     (Object_Logic.full_atomize_tac
-     THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
+     THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))  
      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
 
 fun mk_eqvt_goal pi const arg =
@@ -498,7 +498,7 @@
     in
       Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
         prove_eqvt_tac insts ind_thms const_names simps context)
-      |> ProofContext.export ctxt'' ctxt
+      |> Proof_Context.export ctxt'' ctxt
     end
 
 

--- a/Nominal/nominal_eqvt.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_eqvt.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -32,7 +32,7 @@
 
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cpi = Thm.cterm_of thy (mk_minus pi)
     val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
     val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
@@ -104,7 +104,7 @@
     Goal.prove ctxt' [] [] goal 
       (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
       |> Datatype_Aux.split_conj_thm 
-      |> ProofContext.export ctxt' ctxt
+      |> Proof_Context.export ctxt' ctxt
       |> map (fn th => th RS mp)
       |> map zero_var_indexes
   end
@@ -122,7 +122,7 @@
 
 fun equivariance_cmd pred_name ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ({names, ...}, {preds, raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
     val thms = raw_equivariance preds raw_induct intrs ctxt 

--- a/Nominal/nominal_function.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_function.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -91,7 +91,7 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"})
+      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort "pt"})
       orelse error (cat_lines
       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
@@ -184,7 +184,8 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info, 
-         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
+         lthy |> Local_Theory.declaration {syntax = false, pervasive = false} 
+           (add_function_data o morph_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')

--- a/Nominal/nominal_function_core.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -70,7 +70,7 @@
 
 
 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
-  ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+  ClauseContext { ctxt = Proof_Context.transfer thy ctxt,
     qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
 
 
@@ -202,7 +202,7 @@
     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
-    val thy = ProofContext.theory_of ctxt'
+    val thy = Proof_Context.theory_of ctxt'
 
     fun inst t = subst_bounds (rev qs, t)
     val gs = map inst pre_gs
@@ -240,7 +240,7 @@
     val Globals {h, ...} = globals
 
     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
 
     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
     val lGI = GIntro_thm
@@ -260,7 +260,7 @@
           HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
           |> fold_rev (Logic.all o Free) rcfix
-          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+          |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
           |> abstract_over_list (rev qs)
       in
         RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
@@ -532,7 +532,7 @@
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
   let
     val Globals {h, domT, ranT, x, ...} = globals
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
     val ihyp = Term.all domT $ Abs ("z", domT,
@@ -605,7 +605,7 @@
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
@@ -852,7 +852,7 @@
 (* FIXME: broken by design *)
 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
       qglr = (oqs, _, _, _), ...} = clause
     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
@@ -1014,8 +1014,8 @@
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
-    val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
-    val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+    val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
+    val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
@@ -1023,10 +1023,10 @@
     val (_, lthy) =
       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 
-    val newthy = ProofContext.theory_of lthy
+    val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
 
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
 
     val xclauses = PROFILE "xclauses"
       (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees

--- a/Nominal/nominal_induct.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_induct.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -57,7 +57,7 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
+       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;
@@ -86,7 +86,7 @@
 
 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
@@ -117,10 +117,10 @@
               Method.insert_tac (more_facts @ adefs) THEN'
                 (if simp then
                    Induct.rotate_tac k (length adefs) THEN'
-                   Induct.fix_tac defs_ctxt k
+                   Induct.arbitrary_tac defs_ctxt k
                      (List.partition (member op = frees) xs |> op @)
                  else
-                   Induct.fix_tac defs_ctxt k xs)
+                   Induct.arbitrary_tac defs_ctxt k xs)
             end)
           THEN' Induct.inner_atomize_tac) j))
         THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
@@ -129,7 +129,7 @@
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
                 (Tactic.rtac (rename_params_rule false [] rule') i THEN
-                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
+                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
         else K all_tac)

--- a/Nominal/nominal_inductive.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -170,7 +170,7 @@
 fun non_binder_tac prem intr_cvars Ps ctxt = 
   Subgoal.SUBPROOF (fn {context, params, prems, ...} =>
     let
-      val thy = ProofContext.theory_of context
+      val thy = Proof_Context.theory_of context
       val (prms, p, _) = split_last2 (map snd params)
       val prm_tys = map (fastype_of o term_of) prms
       val cperms = map (cterm_of thy o perm_const) prm_tys
@@ -223,7 +223,7 @@
 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = 
   Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
     let
-      val thy = ProofContext.theory_of ctxt
+      val thy = Proof_Context.theory_of ctxt
       val (prms, p, c) = split_last2 (map snd params)
       val prm_trms = map term_of prms
       val prm_tys = map fastype_of prm_trms
@@ -273,7 +273,7 @@
                     eqvt_stac context,
                     rtac prem',
                     RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
-        |> singleton (ProofContext.export ctxt' ctxt)        
+        |> singleton (Proof_Context.export ctxt' ctxt)        
     in
       rtac side_thm 1
     end) ctxt
@@ -300,7 +300,7 @@
 
 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt
 
     val (ind_prems, ind_concl) = raw_induct'
@@ -357,7 +357,7 @@
       let
         val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' 
         (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) 
-          |> singleton (ProofContext.export ctxt ctxt_outside)
+          |> singleton (Proof_Context.export ctxt ctxt_outside)
           |> Datatype_Aux.split_conj_thm
           |> map (fn thm => thm RS normalise)
           |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) 
@@ -383,7 +383,7 @@
 
 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name);
 

--- a/Nominal/nominal_library.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_library.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -154,7 +154,7 @@
 
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+  Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort at_base})
 
 fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty
   | is_atom_set _ _ = false;

--- a/Nominal/nominal_mutual.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_mutual.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -157,7 +157,7 @@
 
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
 
     val oqnames = map fst pre_qs
     val (qs, _) = Variable.variant_fixes oqnames ctxt
@@ -229,14 +229,14 @@
     Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
       (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
          THEN (asm_full_simp_tac ss 1))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> restore_cond
     |> export
   end
 
 fun mk_applied_form ctxt caTs thm =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
     fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
@@ -247,7 +247,7 @@
 
 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
   let
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
     val newPs =
       map2 (fn Pname => fn MutualPart {cargTs, ...} =>
           Free (Pname, cargTs ---> HOLogic.boolT))
@@ -340,7 +340,7 @@
   in
     Goal.prove ctxt' (flat arg_namess) [] goal
       (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> split_conj_thm
     |> map (fn th => th RS mp)
   end

--- a/Nominal/nominal_termination.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_termination.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -71,7 +71,8 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+               |> Local_Theory.declaration {syntax = false, pervasive = false}
+                    (add_function_data o morph_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end

--- a/Nominal/nominal_thmdecls.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_thmdecls.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -156,7 +156,7 @@
         val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
       in
         Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
-        |> singleton (ProofContext.export ctxt' ctxt)
+        |> singleton (Proof_Context.export ctxt' ctxt)
         |> safe_mk_equiv
         |> zero_var_indexes
       end
@@ -167,7 +167,7 @@
 
 fun eqvt_transform_imp_tac ctxt p p' thm = 
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cp = Thm.cterm_of thy p
     val cp' = Thm.cterm_of thy (mk_minus p')
     val thm' = Drule.cterm_instantiate [(cp, cp')] thm
@@ -199,7 +199,7 @@
       in
         Goal.prove ctxt' [] [] goal'
           (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) 
-        |> singleton (ProofContext.export ctxt' ctxt)
+        |> singleton (Proof_Context.export ctxt' ctxt)
       end
   end