src/HOL/Tools/Function/scnp_reconstruct.ML

   end
 
 (* General reduction pair application *)
 fun rem_inv_img ctxt =
   let
-    val unfold_tac = LocalDefs.unfold_tac ctxt
+    val unfold_tac = Local_Defs.unfold_tac ctxt
   in
     rtac @{thm subsetI} 1
     THEN etac @{thm CollectE} 1
     THEN REPEAT (etac @{thm exE} 1)
     THEN unfold_tac @{thms inv_image_def}

                   else if qs = lq then rtac wmsI2'' 1
                   else rtac wmsI1 1)
             THEN mset_pwleq_tac 1
             THEN EVERY (map2 (less_proof false) qs ps)
             THEN (if strict orelse qs <> lq
-                  then LocalDefs.unfold_tac ctxt set_of_simps
+                  then Local_Defs.unfold_tac ctxt set_of_simps
                        THEN steps_tac MAX true
                        (subtract (op =) qs lq) (subtract (op =) ps lp)
                   else all_tac)
           end
       in

          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)
-         THEN LocalDefs.unfold_tac ctxt
+         THEN Local_Defs.unfold_tac ctxt
            (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
          THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
          THEN EVERY (map (prove_lev true) sl)
          THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
     end