src/HOL/Tools/Function/scnp_reconstruct.ML

 end
 
 structure ScnpReconstruct : SCNP_RECONSTRUCT =
 struct
 
-val PROFILE = FundefCommon.PROFILE
-fun TRACE x = if ! FundefCommon.profile then tracing x else ()
+val PROFILE = Function_Common.PROFILE
+fun TRACE x = if ! Function_Common.profile then tracing x else ()
 
 open ScnpSolve
 
 val natT = HOLogic.natT
 val nat_pairT = HOLogic.mk_prodT (natT, natT)

    wmsI2'' : thm,
    wmsI1 : thm,
    reduction_pair : thm
   }
 
-structure MultisetSetup = TheoryDataFun
+structure Multiset_Setup = TheoryDataFun
 (
   type T = multiset_setup option
   val empty = NONE
   val copy = I;
   val extend = I;
   fun merge _ (v1, v2) = if is_some v2 then v2 else v1
 )
 
-val multiset_setup = MultisetSetup.put o SOME
+val multiset_setup = Multiset_Setup.put o SOME
 
 fun undef x = error "undef"
-fun get_multiset_setup thy = MultisetSetup.get thy
+fun get_multiset_setup thy = Multiset_Setup.get thy
   |> the_default (Multiset
 { msetT = undef, mk_mset=undef,
   mset_regroup_conv=undef, mset_member_tac = undef,
   mset_nonempty_tac = undef, mset_pwleq_tac = undef,
   set_of_simps = [],reduction_pair = refl,

       map_index pt_lev lev
         |> Termination.mk_sumcases D (setT nat_pairT)
         |> cterm_of thy
     in
       PROFILE "Proof Reconstruction"
-        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
+        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv 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)
          THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
          THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)

 end
 
 
 fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
   let
-    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
+    val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
     val orders' = if ms_configured then orders
                   else filter_out (curry op = MS) orders
     val gp = gen_probl D cs
 (*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
     val certificate = generate_certificate use_tags orders' gp

   in
     TERMINATION ctxt (strategy err_cont err_cont)
   end
 
 fun gen_sizechange_tac orders autom_tac ctxt err_cont =
-  TRY (FundefCommon.apply_termination_rule ctxt 1)
+  TRY (Function_Common.apply_termination_rule ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
   THEN
    (rtac @{thm wf_empty} 1
     ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
 
 fun sizechange_tac ctxt autom_tac =
   gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
 
 fun decomp_scnp orders ctxt =
   let
-    val extra_simps = FundefCommon.Termination_Simps.get ctxt
+    val extra_simps = Function_Common.Termination_Simps.get ctxt
     val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
   in
     SIMPLE_METHOD
       (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
   end