src/HOL/Tools/function_package/scnp_reconstruct.ML
changeset 30607 c3d1590debd8
parent 30510 4120fc59dd85
child 30686 47a32dd1b86e
     1.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -291,7 +291,7 @@
     1.4           THEN (rtac @{thm rp_inv_image_rp} 1)
     1.5           THEN (rtac (order_rpair ms_rp label) 1)
     1.6           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
     1.7 -         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
     1.8 +         THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
     1.9           THEN LocalDefs.unfold_tac ctxt
    1.10             (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
    1.11           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
    1.12 @@ -395,7 +395,7 @@
    1.13  
    1.14  fun gen_sizechange_tac orders autom_tac ctxt err_cont =
    1.15    TRY (FundefCommon.apply_termination_rule ctxt 1)
    1.16 -  THEN TRY Termination.wf_union_tac
    1.17 +  THEN TRY (Termination.wf_union_tac ctxt)
    1.18    THEN
    1.19     (rtac @{thm wf_empty} 1
    1.20      ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)