diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_quot.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -58,7 +58,7 @@
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
   let
     val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
-    val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, false, NONE))) qtys_descr qty_args1
+    val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1
     val qty_args3 = qty_args2 ~~ alpha_equivp_thms
   in
     fold_map Quotient_Type.add_quotient_type qty_args3 lthy
@@ -113,9 +113,9 @@
       map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
       |> Variable.exportT lthy3 lthy2
 
-    fun tac _ =
-      Class.intro_classes_tac [] THEN
-        (ALLGOALS (resolve_tac lifted_perm_laws))
+    fun tac ctxt =
+      Class.intro_classes_tac ctxt [] THEN
+        (ALLGOALS (resolve_tac ctxt lifted_perm_laws))
   in
     lthy2
     |> Class.prove_instantiation_exit tac 
@@ -126,7 +126,7 @@
 (* defines the size functions and proves size-class *)
 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
   let
-    val tac = K (Class.intro_classes_tac [])
+    fun tac ctxt = Class.intro_classes_tac ctxt []
   in
     lthy
     |> Local_Theory.exit_global
@@ -157,7 +157,7 @@
   let
     fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
 
-    val vars = Term.add_vars (prop_of thm) []
+    val vars = Term.add_vars (Thm.prop_of thm) []
     val vars' = map (Var o unraw_var_str) vars
   in
     Thm.certify_instantiate ([], (vars ~~ vars')) thm
@@ -229,14 +229,14 @@
 
     val tac = 
       EVERY' [ rtac @{thm supports_finite},
-               resolve_tac qsupports_thms,
+               resolve_tac ctxt' qsupports_thms,
                asm_simp_tac (put_simpset HOL_ss ctxt'
                 addsimps @{thms finite_supp supp_Pair finite_Un}) ]
   in
     Goal.prove ctxt' [] [] goals
       (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
     |> singleton (Proof_Context.export ctxt' ctxt)
-    |> Datatype_Aux.split_conj_thm
+    |> Old_Datatype_Aux.split_conj_thm
     |> map zero_var_indexes
   end
 
@@ -250,9 +250,9 @@
       |> Local_Theory.exit_global
       |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
   
-    fun tac _ =
-      Class.intro_classes_tac [] THEN
-        (ALLGOALS (resolve_tac qfsupp_thms))
+    fun tac ctxt =
+      Class.intro_classes_tac ctxt [] THEN
+        (ALLGOALS (resolve_tac ctxt qfsupp_thms))
   in
     lthy1
     |> Class.prove_instantiation_exit tac 
@@ -303,7 +303,7 @@
 
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def 
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def 
   prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 
 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
@@ -436,7 +436,7 @@
       | Const (@{const_name "Abs_res"}, _) => true
       | _ => false
   in 
-    thm |> prop_of 
+    thm |> Thm.prop_of 
         |> HOLogic.dest_Trueprop
         |> HOLogic.dest_eq
         |> fst
@@ -538,8 +538,8 @@
   
         val tac1 = 
           if rec_flag
-          then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
-          else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
+          then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+          else resolve_tac ctxt @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
         
         val tac2 =
           EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss),
@@ -559,10 +559,10 @@
   let
     fun aux_tac prem bclauses =
       case (get_all_binders bclauses) of
-        [] => EVERY' [rtac prem, atac]
+        [] => EVERY' [rtac prem, assume_tac ctxt]
       | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  
           let
-            val parms = map (term_of o snd) params
+            val parms = map (Thm.term_of o snd) params
             val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
   
             val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
@@ -572,7 +572,7 @@
                             REPEAT o (etac @{thm conjE})]) [fthm] ctxt
   
             val abs_eq_thms = flat 
-             (map (abs_eq_thm ctxt' fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses)
+             (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
 
             val ((_, eqs), ctxt'') = Obtain.result
               (fn ctxt'' => EVERY1 
@@ -592,17 +592,17 @@
             val tac1 = SOLVED' (EVERY'
               [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
                 rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
-                conj_tac (DETERM o resolve_tac fprops') ]) 
+                conj_tac (DETERM o resolve_tac ctxt'' fprops') ]) 
 
             (* for equalities between constructors *)
             val tac2 = SOLVED' (EVERY' 
               [ rtac (@{thm ssubst} OF prems),
                 rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
                 rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
-                conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) 
+                conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
 
             (* proves goal "P" *)
-            val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+            val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
               (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
               |> singleton (Proof_Context.export ctxt'' ctxt)  
           in
@@ -622,7 +622,7 @@
     val c = Free (c, TFree (a, @{sort fs}))
 
     val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
-      |> map prop_of
+      |> map Thm.prop_of
       |> map Logic.strip_horn
       |> split_list
 
@@ -707,7 +707,7 @@
     val c = Free (c_name, c_ty)
 
     val (prems, concl) = induct'
-      |> prop_of
+      |> Thm.prop_of
       |> Logic.strip_horn 
 
     val concls = concl
@@ -721,13 +721,12 @@
       |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
 
     fun pat_tac ctxt thm =
-      Subgoal.FOCUS (fn {params, context, ...} => 
+      Subgoal.FOCUS (fn {params, context = ctxt', ...} => 
         let
-          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 ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
+          val vs = Term.add_vars (Thm.prop_of thm) []
           val vs_tys = map (Type.legacy_freeze_type o snd) vs
-          val vs_ctrms = map (cterm_of thy o Var) vs
+          val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
           val assigns = map (lookup ty_parms) vs_tys          
           
           val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
@@ -739,7 +738,7 @@
     fun size_simp_tac ctxt = 
       simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms))
   in
-    Goal.prove_multi lthy'' [] prems' concls
+    Goal.prove_common lthy'' NONE [] prems' concls
       (fn {prems, context = ctxt} => 
         Induction_Schema.induction_schema_tac ctxt prems  
         THEN RANGE (map (pat_tac ctxt) exhausts) 1