--- a/src/CCL/CCL.thy Fri Jul 24 20:55:56 2009 +0200
+++ b/src/CCL/CCL.thy Fri Jul 24 21:02:34 2009 +0200
@@ -256,12 +256,12 @@
val ccl_dstncts =
let fun mk_raw_dstnct_thm rls s =
- prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
+ OldGoals.prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
in map (mk_raw_dstnct_thm caseB_lemmas)
(mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
fun mk_dstnct_thms thy defs inj_rls xs =
- let fun mk_dstnct_thm rls s = prove_goalw thy defs s
+ let fun mk_dstnct_thm rls s = OldGoals.prove_goalw thy defs s
(fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end