src/CCL/CCL.thy
changeset 32174 9036cc8ae775
parent 32154 9721e8e4d48c
child 32175 a89979440d2c
--- 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