src/Tools/case_product.ML
changeset 42361 23f352990944
parent 41883 392364739e5d
child 44045 2814ff2a6e3e
     1.1 --- a/src/Tools/case_product.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/Tools/case_product.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4      (Tactic.rtac (thm1 OF p_cons1)
     1.5       THEN' EVERY' (map (fn p =>
     1.6         Tactic.rtac thm2'
     1.7 -       THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss)
     1.8 +       THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
     1.9      )
    1.10    end
    1.11