diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jul 09 02:32:46 2015 +0100
@@ -5,7 +5,7 @@
     Nominal Isabelle. 
 *)
 theory Nominal2_Base
-imports Main 
+imports "~~/src/HOL/Library/Old_Datatype"
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
         "~~/src/HOL/Library/FinFun"
@@ -769,9 +769,8 @@
 subsection {* Eqvt infrastructure *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw}. *}
-
+                   
 ML_file "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
 
 
 lemmas [eqvt] =
@@ -823,7 +822,7 @@
  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
 
 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ctxt => fn ctrm =>
-  case term_of (Thm.dest_arg ctrm) of 
+  case Thm.term_of (Thm.dest_arg ctrm) of 
     Free _ => NONE
   | Var _ => NONE
   | Const (@{const_name permute}, _) $ _ $ _ => NONE
@@ -891,14 +890,14 @@
   shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)"
   by (simp add: permute_bool_def)
 
-declare imp_eqvt[folded induct_implies_def, eqvt]
+declare imp_eqvt[folded HOL.induct_implies_def, eqvt]
 
 lemma all_eqvt [eqvt]:
   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
   unfolding All_def
   by (perm_simp) (rule refl)
 
-declare all_eqvt[folded induct_forall_def, eqvt]
+declare all_eqvt[folded HOL.induct_forall_def, eqvt]
 
 lemma ex_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
@@ -1885,17 +1884,18 @@
 
 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ctxt => fn ctrm =>
   let 
-    val _ $ _ $ f = term_of ctrm
+    val _ $ _ $ f = Thm.term_of ctrm
   in
     case (Term.add_frees f [], Term.add_vars f []) of
       ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]})
-    | (x::_, []) => let
-         val thy = Proof_Context.theory_of ctxt
-         val argx = Free x
-         val absf = absfree x f
-         val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))]
-         val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] 
-         val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+    | (x::_, []) =>
+      let
+        val argx = Free x
+        val absf = absfree x f
+        val cty_inst =
+          [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
+        val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] 
+        val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
       in
         SOME(thm RS @{thm Eq_TrueI}) 
       end  
@@ -2952,7 +2952,7 @@
 
 
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
-  case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
+  case Thm.term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
     let  
       fun first_is_neg lhs rhs [] = NONE
         | first_is_neg lhs rhs (thm::thms) =
@@ -2973,8 +2973,8 @@
                member (op=) atms lhs andalso member (op=) atms rhs
              end) 
             | _ => false)
-         |> map (simplify (put_simpset HOL_basic_ss  ctxt addsimps simp_thms))
-         |> map HOLogic.conj_elims
+         |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms))
+         |> map (HOLogic.conj_elims ctxt)
          |> flat
     in 
       case first_is_neg lhs rhs prems of
@@ -3353,7 +3353,7 @@
 
 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm =>
   let
-     val _ $ h = term_of ctrm
+     val _ $ h = Thm.term_of ctrm
 
      val cfresh = @{const_name fresh}
      val catom  = @{const_name atom}