src/Tools/case_product.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 58826 2ed2eaabe3df
     1.1 --- a/src/Tools/case_product.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Tools/case_product.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -65,14 +65,14 @@
     1.4      (concl, prems)
     1.5    end
     1.6  
     1.7 -fun case_product_tac prems struc thm1 thm2 =
     1.8 +fun case_product_tac ctxt prems struc thm1 thm2 =
     1.9    let
    1.10      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    1.11      val thm2' = thm2 OF p_cons2
    1.12    in
    1.13      rtac (thm1 OF p_cons1)
    1.14       THEN' EVERY' (map (fn p =>
    1.15 -       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
    1.16 +       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
    1.17    end
    1.18  
    1.19  fun combine ctxt thm1 thm2 =
    1.20 @@ -80,8 +80,9 @@
    1.21      val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
    1.22      val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
    1.23    in
    1.24 -    Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
    1.25 -      case_product_tac prems prems_rich i_thm1 i_thm2 1)
    1.26 +    Goal.prove ctxt' [] (flat prems_rich) concl
    1.27 +      (fn {context = ctxt'', prems} =>
    1.28 +        case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
    1.29      |> singleton (Variable.export ctxt' ctxt)
    1.30    end
    1.31