tuned;
authorwenzelm
Tue Nov 08 11:44:37 2011 +0100 (2011-11-08)
changeset 454037a0b8debef77
parent 45402 1fac64bbdb4f
child 45404 69ec395ef6ca
tuned;
src/HOL/Library/reflection.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Tue Nov 08 08:56:24 2011 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Tue Nov 08 11:44:37 2011 +0100
     1.3 @@ -60,10 +60,11 @@
     1.4     fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
     1.5       | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
     1.6     fun tryext x = (x RS ext2 handle THM _ =>  x)
     1.7 -   val cong = (Goal.prove ctxt'' [] (map mk_def env)
     1.8 -                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
     1.9 -                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
    1.10 -                                                        THEN rtac th' 1)) RS sym
    1.11 +   val cong =
    1.12 +    (Goal.prove ctxt'' [] (map mk_def env)
    1.13 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    1.14 +      (fn {context, prems, ...} =>
    1.15 +        Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
    1.16  
    1.17     val (cong' :: vars') =
    1.18         Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
     2.1 --- a/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 08:56:24 2011 +0100
     2.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 11:44:37 2011 +0100
     2.3 @@ -176,7 +176,7 @@
     2.4    end
     2.5  
     2.6  fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
     2.7 -  import (export : thm -> thm) sum_psimp_eq =
     2.8 +    import (export : thm -> thm) sum_psimp_eq =
     2.9    let
    2.10      val (MutualPart {f=SOME f, ...}) = get_part fname parts
    2.11  
    2.12 @@ -190,9 +190,10 @@
    2.13    in
    2.14      Goal.prove ctxt [] []
    2.15        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
    2.16 -      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
    2.17 -         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    2.18 -         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
    2.19 +      (fn _ =>
    2.20 +        Local_Defs.unfold_tac ctxt all_orig_fdefs
    2.21 +          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    2.22 +          THEN (simp_tac (simpset_of ctxt)) 1)
    2.23      |> restore_cond
    2.24      |> export
    2.25    end
     3.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 08:56:24 2011 +0100
     3.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 11:44:37 2011 +0100
     3.3 @@ -64,7 +64,7 @@
     3.4  
     3.5  (*rewrite conclusion with k-th assumtion*)
     3.6  fun rewrite_with_asm_tac ctxt k =
     3.7 -  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
     3.8 +  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
     3.9      Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
    3.10  
    3.11  fun dest_case thy t =