# HG changeset patch
# User wenzelm
# Date 1248463085 -7200
# Node ID a89979440d2c6fd37595958877125badee65dcc6
# Parent  9036cc8ae7757cb13da2ebdb3efe06a52626d7ca
eliminated OldGoals.prove_goal;

diff -r 9036cc8ae775 -r a89979440d2c src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Fri Jul 24 21:02:34 2009 +0200
+++ b/src/CCL/CCL.thy	Fri Jul 24 21:18:05 2009 +0200
@@ -255,14 +255,20 @@
 val caseB_lemmas = mk_lemmas @{thms caseBs}
 
 val ccl_dstncts =
-        let fun mk_raw_dstnct_thm rls s =
-                  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
+  let
+    fun mk_raw_dstnct_thm rls s =
+      Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
+        (fn _=> rtac notI 1 THEN 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 = OldGoals.prove_goalw thy defs s
-    (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
+  let
+    fun mk_dstnct_thm rls s =
+      Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
+        (fn _ =>
+          rewrite_goals_tac defs THEN
+          simp_tac (global_simpset_of thy addsimps (rls @ inj_rls)) 1)
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
 fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss