diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_inductive.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -35,7 +35,7 @@
   | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t
   | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t
   | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
-  | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
+  | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t
   | real_head_of t = head_of t
 
 
@@ -81,7 +81,7 @@
   end
 
 fun induct_forall_const T =
-  Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})
+  Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool})
 
 fun mk_induct_forall (a, T) t =
   induct_forall_const T $ Abs (a, T, t)
@@ -156,7 +156,7 @@
 val all_elims = 
   let
     fun spec' ct =
-      Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}
+      Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
   in
     fold (fn ct => fn th => th RS spec' ct)
   end
@@ -172,34 +172,33 @@
         |> flag ? (all_elims [p])
         |> flag ? (eqvt_srule context)
     in
-      asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms induct_forall_def})) 1
+      asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
     end) ctxt
 
 fun non_binder_tac prem intr_cvars Ps ctxt = 
-  Subgoal.SUBPROOF (fn {context, params, prems, ...} =>
+  Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} =>
     let
-      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
+      val prm_tys = map (fastype_of o Thm.term_of) prms
+      val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
       val prem' = prem
         |> cterm_instantiate (intr_cvars ~~ p_prms) 
         |> eqvt_srule ctxt
 
       (* for inductive-premises*)
-      fun tac1 prm = helper_tac true prm p context 
+      fun tac1 prm = helper_tac true prm p ctxt'
 
       (* for non-inductive premises *)   
       fun tac2 prm =  
         EVERY' [ minus_permute_intro_tac p, 
-                 eqvt_stac context, 
-                 helper_tac false prm p context ]
+                 eqvt_stac ctxt', 
+                 helper_tac false prm p ctxt' ]
 
       fun select prm (t, i) =
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
     in
-      EVERY1 [ eqvt_stac context, 
+      EVERY1 [ eqvt_stac ctxt', 
                rtac prem', 
                RANGE (map (SUBGOAL o select) prems) ]
     end) ctxt
@@ -232,9 +231,8 @@
 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 = Proof_Context.theory_of ctxt
       val (prms, p, c) = split_last2 (map snd params)
-      val prm_trms = map term_of prms
+      val prm_trms = map Thm.term_of prms
       val prm_tys = map fastype_of prm_trms
 
       val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm 
@@ -243,7 +241,7 @@
       val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
         |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
       
-      val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm'
+      val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
 
       val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
               (K (EVERY1 [etac @{thm exE}, 
@@ -256,7 +254,7 @@
       val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
       fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
 
-      val cperms = map (cterm_of thy o perm_const) prm_tys
+      val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 
       val prem' = prem
         |> cterm_instantiate (intr_cvars ~~ qp_prms)
@@ -277,13 +275,13 @@
       fun select prm (t, i) =
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
 
-      val side_thm = Goal.prove ctxt' [] [] (term_of concl)
-        (fn {context, ...} => 
-           EVERY1 [ CONVERSION (expand_conv_bot context),
-                    eqvt_stac context,
+      val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl)
+        (fn {context = ctxt'', ...} => 
+           EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
+                    eqvt_stac ctxt'',
                     rtac prem',
                     RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
-        |> singleton (Proof_Context.export ctxt' ctxt)        
+        |> singleton (Proof_Context.export ctxt' ctxt)
     in
       rtac side_thm 1
     end) ctxt
@@ -310,23 +308,22 @@
 
 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt
 
     val (ind_prems, ind_concl) = raw_induct'
-      |> prop_of
+      |> Thm.prop_of
       |> Logic.strip_horn
       |>> map strip_full_horn
     val params = map (fn (x, _, _) => x) ind_prems
     val param_trms = (map o map) Free params  
 
-    val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs
+    val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs
     val intr_vars = (map o map) fst intr_vars_tys
     val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms
-    val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys      
+    val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys
 
     val (intr_prems, intr_concls) = intrs
-      |> map prop_of
+      |> map Thm.prop_of
       |> map2 subst_Vars intr_vars_substs
       |> map Logic.strip_horn
       |> split_list
@@ -369,7 +366,7 @@
         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 (Proof_Context.export ctxt ctxt_outside)
-          |> Datatype_Aux.split_conj_thm
+          |> Old_Datatype_Aux.split_conj_thm
           |> map (fn thm => thm RS normalise)
           |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt
               addsimps @{thms permute_zero induct_rulify})) 
@@ -417,7 +414,7 @@
       let
         (* fixme hack *)
         val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt
-        val trms = map (term_of o snd) ctrms
+        val trms = map (Thm.term_of o snd) ctrms
         val ctxt'' = fold Variable.declare_term trms ctxt'
       in
         map (Syntax.read_term ctxt'') avoid_trms
@@ -439,7 +436,7 @@
   val main_parser = Parse.xname -- avoids_parser
 in
   val _ =
-    Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+    Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
       "prove strong induction theorem for inductive predicate involving nominal datatypes"
         (main_parser >> prove_strong_inductive_cmd)
 end