src/CCL/CCL.thy
changeset 32175 a89979440d2c
parent 32174 9036cc8ae775
child 35409 5c5bb83f2bae
     1.1 --- a/src/CCL/CCL.thy	Fri Jul 24 21:02:34 2009 +0200
     1.2 +++ b/src/CCL/CCL.thy	Fri Jul 24 21:18:05 2009 +0200
     1.3 @@ -255,14 +255,20 @@
     1.4  val caseB_lemmas = mk_lemmas @{thms caseBs}
     1.5  
     1.6  val ccl_dstncts =
     1.7 -        let fun mk_raw_dstnct_thm rls s =
     1.8 -                  OldGoals.prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
     1.9 -        in map (mk_raw_dstnct_thm caseB_lemmas)
    1.10 -                (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.11 +  let
    1.12 +    fun mk_raw_dstnct_thm rls s =
    1.13 +      Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
    1.14 +        (fn _=> rtac notI 1 THEN eresolve_tac rls 1)
    1.15 +  in map (mk_raw_dstnct_thm caseB_lemmas)
    1.16 +    (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.17  
    1.18  fun mk_dstnct_thms thy defs inj_rls xs =
    1.19 -  let fun mk_dstnct_thm rls s = OldGoals.prove_goalw thy defs s
    1.20 -    (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
    1.21 +  let
    1.22 +    fun mk_dstnct_thm rls s =
    1.23 +      Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
    1.24 +        (fn _ =>
    1.25 +          rewrite_goals_tac defs THEN
    1.26 +          simp_tac (global_simpset_of thy addsimps (rls @ inj_rls)) 1)
    1.27    in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    1.28  
    1.29  fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss