src/HOL/Tools/Predicate_Compile/core_data.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 55437 3fd63b92ea3b
     1.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -219,8 +219,8 @@
     1.4            |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
     1.5          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
     1.6          val case_th =
     1.7 -          rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
     1.8 -        val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
     1.9 +          rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    1.10 +        val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
    1.11          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
    1.12          val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
    1.13            OF (replicate nargs @{thm refl})
    1.14 @@ -236,7 +236,7 @@
    1.15        (PEEK nprems_of
    1.16          (fn n =>
    1.17            ALLGOALS (fn i =>
    1.18 -            rewrite_goal_tac [@{thm split_paired_all}] i
    1.19 +            rewrite_goal_tac ctxt [@{thm split_paired_all}] i
    1.20              THEN (SUBPROOF (instantiate i n) ctxt i))))
    1.21    in
    1.22      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)