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