# HG changeset patch
# User wenzelm
# Date 1425668925 -3600
# Node ID aacdce52b2fce4f0b110a3b4a2c49c41026db377
# Parent  6c0e70b011118b8adf4f1c8bd0de2fa24b488ba3
proper context;

diff -r 6c0e70b01111 -r aacdce52b2fc src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Mar 06 18:21:32 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Mar 06 20:08:45 2015 +0100
@@ -1917,9 +1917,9 @@
   val mset_nonempty_tac =
       rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
 
-  val regroup_munion_conv =
-      Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
-        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
+  fun regroup_munion_conv ctxt =
+    Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
+      (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
 
   fun unfold_pwleq_tac i =
     (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
diff -r 6c0e70b01111 -r aacdce52b2fc src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 18:21:32 2015 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 20:08:45 2015 +0100
@@ -21,8 +21,8 @@
   val try_proof: cterm -> tactic -> proof_attempt
 
   val dest_binop_list: string -> term -> term list
-  val regroup_conv: string -> string -> thm list -> int list -> conv
-  val regroup_union_conv: int list -> conv
+  val regroup_conv: Proof.context -> string -> string -> thm list -> int list -> conv
+  val regroup_union_conv: Proof.context -> int list -> conv
 
   val inst_constrs_of: Proof.context -> typ -> term list
 end
@@ -93,11 +93,8 @@
         (e.g. [0,1,3] in the above example)
 *)
 
-fun regroup_conv neu cn ac is ct =
+fun regroup_conv ctxt neu cn ac is ct =
  let
-   val thy = Thm.theory_of_cterm ct
-   val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
-
    val mk = HOLogic.mk_binop cn
    val t = Thm.term_of ct
    val xs = dest_binop_list cn t
@@ -117,8 +114,8 @@
  end
 
 (* instance for unions *)
-val regroup_union_conv =
-  regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}
+fun regroup_union_conv ctxt =
+  regroup_conv ctxt @{const_abbrev Set.empty} @{const_name Lattices.sup}
     (map (fn t => t RS eq_reflection)
       (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
 
diff -r 6c0e70b01111 -r aacdce52b2fc src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 18:21:32 2015 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 20:08:45 2015 +0100
@@ -16,7 +16,7 @@
     {
      msetT : typ -> typ,
      mk_mset : typ -> term list -> term,
-     mset_regroup_conv : int list -> conv,
+     mset_regroup_conv : Proof.context -> int list -> conv,
      mset_member_tac : int -> int -> tactic,
      mset_nonempty_tac : int -> tactic,
      mset_pwleq_tac : int -> tactic,
@@ -48,7 +48,7 @@
   {
    msetT : typ -> typ,
    mk_mset : typ -> term list -> term,
-   mset_regroup_conv : int list -> conv,
+   mset_regroup_conv : Proof.context -> int list -> conv,
    mset_member_tac : int -> int -> tactic,
    mset_nonempty_tac : int -> tactic,
    mset_pwleq_tac : int -> tactic,
@@ -71,7 +71,7 @@
 
 fun undef _ = error "undef"
 
-fun get_multiset_setup thy = Multiset_Setup.get thy
+fun get_multiset_setup ctxt = Multiset_Setup.get (Proof_Context.theory_of ctxt)
   |> the_default (Multiset
     { msetT = undef, mk_mset=undef,
       mset_regroup_conv=undef, mset_member_tac = undef,
@@ -145,12 +145,11 @@
 
 fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
   let
-    val thy = Proof_Context.theory_of ctxt
     val Multiset
           { msetT, mk_mset,
             mset_regroup_conv, mset_pwleq_tac, set_of_simps,
             smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
-        = get_multiset_setup thy
+        = get_multiset_setup ctxt
 
     fun measure_fn p = nth (Termination.get_measures D p)
 
@@ -239,8 +238,8 @@
                 fun t_conv a C =
                   params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
                 val goal_rewrite =
-                    t_conv arg1_conv (mset_regroup_conv iqs)
-                    then_conv t_conv arg_conv (mset_regroup_conv ips)
+                    t_conv arg1_conv (mset_regroup_conv ctxt iqs)
+                    then_conv t_conv arg_conv (mset_regroup_conv ctxt ips)
                 end
               in
                 CONVERSION goal_rewrite 1
@@ -275,7 +274,7 @@
         |> Thm.cterm_of ctxt
     in
       PROFILE "Proof Reconstruction"
-        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
+        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv ctxt sl))) 1
          THEN (rtac @{thm reduction_pair_lemma} 1)
          THEN (rtac @{thm rp_inv_image_rp} 1)
          THEN (rtac (order_rpair ms_rp label) 1)
diff -r 6c0e70b01111 -r aacdce52b2fc src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 18:21:32 2015 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 20:08:45 2015 +0100
@@ -331,7 +331,7 @@
    val is = map (fn c => find_index (curry op aconv c) cs') cs
  in
    CONVERSION (Conv.arg_conv (Conv.arg_conv
-     (Function_Lib.regroup_union_conv is))) i
+     (Function_Lib.regroup_union_conv ctxt is))) i
  end)