src/CCL/CCL.thy
changeset 32174 9036cc8ae775
parent 32154 9721e8e4d48c
child 32175 a89979440d2c
     1.1 --- a/src/CCL/CCL.thy	Fri Jul 24 20:55:56 2009 +0200
     1.2 +++ b/src/CCL/CCL.thy	Fri Jul 24 21:02:34 2009 +0200
     1.3 @@ -256,12 +256,12 @@
     1.4  
     1.5  val ccl_dstncts =
     1.6          let fun mk_raw_dstnct_thm rls s =
     1.7 -                  prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
     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  
    1.12  fun mk_dstnct_thms thy defs inj_rls xs =
    1.13 -  let fun mk_dstnct_thm rls s = prove_goalw thy defs s
    1.14 +  let fun mk_dstnct_thm rls s = OldGoals.prove_goalw thy defs s
    1.15      (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
    1.16    in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    1.17