changeset 42361 | 23f352990944 |
parent 41128 | bb2fa5c13d1a |
child 42370 | 244911efd275 |
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 16:15:37 2011 +0200 @@ -90,7 +90,7 @@ Seq.maps (fn (names, st) => CASES (Rule_Cases.make_common - (ProofContext.theory_of ctxt, + (Proof_Context.theory_of ctxt, Thm.prop_of (Rule_Cases.internalize_params st)) names) Tactical.all_tac st)) in