src/HOL/HOLCF/Tools/fixrec.ML
changeset 51717 9e7d1c139569
parent 47432 e1576d13e933
child 57945 cacb00a569e0
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4            Syntax.string_of_term lthy prop)
     1.5          val rules = Cont2ContData.get lthy
     1.6          val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
     1.7 -        val slow_tac = SOLVED' (simp_tac (simpset_of lthy))
     1.8 +        val slow_tac = SOLVED' (simp_tac lthy)
     1.9          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
    1.10        in
    1.11          Goal.prove lthy [] [] prop (K tac)
    1.12 @@ -293,7 +293,6 @@
    1.13  fun fixrec_simp_tac ctxt =
    1.14    let
    1.15      val tab = FixrecUnfoldData.get (Context.Proof ctxt)
    1.16 -    val ss = Simplifier.simpset_of ctxt
    1.17      val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls
    1.18      fun tac (t, i) =
    1.19        let
    1.20 @@ -302,7 +301,7 @@
    1.21          val unfold_thm = the (Symtab.lookup tab c)
    1.22          val rule = unfold_thm RS @{thm ssubst_lhs}
    1.23        in
    1.24 -        CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i)
    1.25 +        CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ctxt i)
    1.26        end
    1.27    in
    1.28      SUBGOAL (fn ti => the_default no_tac (try tac ti))
    1.29 @@ -311,9 +310,8 @@
    1.30  (* proves a block of pattern matching equations as theorems, using unfold *)
    1.31  fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
    1.32    let
    1.33 -    val ss = Simplifier.simpset_of ctxt
    1.34      val rule = unfold_thm RS @{thm ssubst_lhs}
    1.35 -    val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1
    1.36 +    val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1
    1.37      fun prove_term t = Goal.prove ctxt [] [] t (K tac)
    1.38      fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t)
    1.39    in