src/HOL/Tools/Function/function_core.ML

       |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
     end
   end
 
 (* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
-  let
+fun mk_replacement_lemma ctxt h ih_elim clause =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
       RCs, tree, ...} = clause
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
     end

     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
     val h_assums = map (fn RCInfo {h_assum, ...} =>
       Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
 
     val (eql, _) =
-      Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
+      Function_Ctx_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
 
     val replace_lemma = (eql RS meta_eq_to_obj_eq)
       |> Thm.implies_intr (cprop_of case_hyp)
       |> fold_rev (Thm.implies_intr o cprop_of) h_assums
       |> fold_rev (Thm.implies_intr o cprop_of) ags

     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
   end
 
 
 
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
-  let
+fun mk_uniqueness_case ctxt globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val Globals {x, y, ranT, fvar, ...} = globals
     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
     val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
-    val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+    val ih_intro_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro
 
     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
       |> fold_rev (Thm.implies_intr o cprop_of) CCas
       |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 

 
     val exactly_one =
       ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
-      |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+      |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
       |> Thm.implies_intr (cprop_of case_hyp)
       |> fold_rev (Thm.implies_intr o cprop_of) ags
       |> fold_rev Thm.forall_intr cqs
 
     val function_value =

     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
 
     val _ = trace_msg (K "Proving Replacement lemmas...")
-    val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+    val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
 
     val _ = trace_msg (K "Proving cases for unique existence...")
     val (ex1s, values) =
-      split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+      split_list
+        (map
+          (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas)
+          clauses)
 
     val _ = trace_msg (K "Proving: Graph is a function")
     val graph_is_function = complete
       |> Thm.forall_elim_vars 0
       |> fold (curry op COMP) ex1s

 
 (**********************************************************
  *                   PROVING THE RULES
  **********************************************************)
 
-fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
-  let
+fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val Globals {domT, z, ...} = globals
 
     fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
       let
         val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)

         |> (fn it => it COMP graph_is_function)
         |> Thm.implies_intr z_smaller
         |> Thm.forall_intr (cterm_of thy z)
         |> (fn it => it COMP valthm)
         |> Thm.implies_intr lhs_acc
-        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
+        |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
         |> fold_rev (Thm.implies_intr o cprop_of) ags
         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
       end
   in
     map2 mk_psimp clauses valthms

 
 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
 val wf_in_rel = @{thm FunDef.wf_in_rel}
 val in_rel_def = @{thm FunDef.in_rel_def}
 
-fun mk_nest_term_case thy globals R' ihyp clause =
-  let
+fun mk_nest_term_case ctxt globals R' ihyp clause =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val Globals {z, ...} = globals
     val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
       qglr=(oqs, _, _, _), ...} = clause
 
-    val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+    val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp
 
     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
       let
         val used = (u @ sub)
           |> map (fn (ctxt, thm) => Function_Ctx_Tree.export_thm thy ctxt thm)

   in
     Function_Ctx_Tree.traverse_tree step tree
   end
 
 
-fun mk_nest_term_rule thy globals R R_cases clauses =
-  let
+fun mk_nest_term_rule ctxt globals R R_cases clauses =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val Globals { domT, x, z, ... } = globals
     val acc_R = mk_acc domT R
 
     val R' = Free ("R", fastype_of R)
 

 
     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
 
     val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
 
-    val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
+    val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
   in
     R_cases
     |> Thm.forall_elim (cterm_of thy z)
     |> Thm.forall_elim (cterm_of thy x)
     |> Thm.forall_elim (cterm_of thy (acc_R $ z))

     |> fold Thm.implies_intr hyps
     |> Thm.implies_intr wfR'
     |> Thm.forall_intr (cterm_of thy R')
     |> Thm.forall_elim (cterm_of thy (inrel_R))
     |> curry op RS wf_in_rel
-    |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
+    |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
     |> Thm.forall_intr (cterm_of thy Rrel)
   end
 
 
 

          compat_store G_elim) f_defthm
 
     fun mk_partial_rules provedgoal =
       let
         val newthy = theory_of_thm provedgoal (*FIXME*)
+        val newctxt = Proof_Context.init_global newthy (*FIXME*)
 
         val (graph_is_function, complete_thm) =
           provedgoal
           |> Conjunction.elim
           |> apfst (Thm.forall_elim_vars 0)
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
 
         val psimps = PROFILE "Proving simplification rules"
-          (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+          (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function
 
         val simple_pinduct = PROFILE "Proving partial induction rule"
           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
 
         val total_intro = PROFILE "Proving nested termination rule"
-          (mk_nest_term_rule newthy globals R R_elim) xclauses
+          (mk_nest_term_rule newctxt globals R R_elim) xclauses
 
         val dom_intros =
           if domintros then SOME (PROFILE "Proving domain introduction rules"
              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
            else NONE