--- a/Nominal/nominal_thmdecls.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_thmdecls.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -62,7 +62,6 @@
   val eqvt_del: attribute
   val eqvt_raw_add: attribute
   val eqvt_raw_del: attribute
-  val setup: theory -> theory
   val get_eqvts_thms: Proof.context -> thm list
   val get_eqvts_raw_thms: Proof.context -> thm list
   val eqvt_transform: Proof.context -> thm -> thm
@@ -91,6 +90,11 @@
 val eqvts = Item_Net.content o EqvtData.get
 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get
 
+val _ =
+  Theory.setup
+   (Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
+    Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw))
+
 val get_eqvts_thms = eqvts o Context.Proof
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof
 
@@ -109,9 +113,9 @@
     fun error_msg () =
       error
         ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^
-         Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+         Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm))
   in
-    case prop_of thm of
+    case Thm.prop_of thm of
       Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
         if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
           c
@@ -151,7 +155,7 @@
   (
     if Item_Net.member (EqvtData.get context) thm then
       warning ("Theorem already declared as equivariant:\n" ^
-        Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+        Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm))
     else ();
     EqvtData.map (Item_Net.update thm) context
   )
@@ -162,7 +166,7 @@
       EqvtData.map (Item_Net.remove thm) context
     else (
       warning ("Cannot delete non-existing equivariance theorem:\n" ^
-        Syntax.string_of_term (Context.proof_of context) (prop_of thm));
+        Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm));
       context
     )
   )
@@ -187,7 +191,7 @@
 
 fun thm_4_of_1 ctxt thm =
   let
-    val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop
+    val (p, c) = thm |> Thm.prop_of |> HOLogic.dest_Trueprop
       |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt)
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
     val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
@@ -209,7 +213,7 @@
   let
     val ss_thms = @{thms "permute_minus_cancel"(2)}
   in
-    EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac,
+    EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
       rtac @{thm "permute_boolI"}, dtac thm', 
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
   end
@@ -218,7 +222,7 @@
 
 fun thm_1_of_2 ctxt thm =
   let
-    val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop
+    val (prem, concl) = thm |> Thm.prop_of |> Logic.dest_implies |> apply2 HOLogic.dest_Trueprop
     (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded
        or tuples, we need the following function to find ?p *)
     fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p
@@ -228,10 +232,9 @@
     val p = concl |> dest_comb |> snd |> find_perm
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
     val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
-    val certify = cterm_of (theory_of_thm thm)
-    val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm
+    val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
   in
-    Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1)
+    Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
       |> singleton (Proof_Context.export ctxt' ctxt)
   end
   handle TERM _ =>
@@ -254,7 +257,7 @@
 
 (* Transforms a theorem of the form (1) or (2) into the form (4). *)
 fun eqvt_transform ctxt thm =
-  (case prop_of thm of @{const "Trueprop"} $ _ =>
+  (case Thm.prop_of thm of @{const "Trueprop"} $ _ =>
     thm_4_of_1 ctxt thm
   | @{const Pure.imp} $ _ $ _ =>
     thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
@@ -268,7 +271,7 @@
    (3)) and (4); transforms a theorem of the form (2) into
    theorems of the form (3) and (4). *)
 fun eqvt_and_raw_transform ctxt thm =
-  (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
+  (case Thm.prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
     let
       val th' =
         if fastype_of c_args = @{typ "bool"}
@@ -310,15 +313,11 @@
 val eqvt_add = eqvt_add_or_del add_thm add_raw_thm
 val eqvt_del = eqvt_add_or_del del_thm del_raw_thm
 
-
-(** setup function **)
-
-val setup =
-  Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
-    "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
-  Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
-    "Declaration of raw equivariance lemmas - no transformation is performed" #>
-  Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
-  Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
+      "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
+    Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
+      "Declaration of raw equivariance lemmas - no transformation is performed")
 
 end;