src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
changeset 57983 6edc3529bb4e
parent 57399 cfc19f0a6261
child 58956 a816aa3ff391
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -54,8 +54,8 @@
     1.4  fun distinct_in_prems_tac distincts =
     1.5    eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
     1.6  
     1.7 -fun mk_primcorec_nchotomy_tac ctxt disc_exhausts =
     1.8 -  HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt);
     1.9 +fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
    1.10 +  HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
    1.11  
    1.12  fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
    1.13    let val ks = 1 upto n in
    1.14 @@ -105,11 +105,11 @@
    1.15  fun prelude_tac ctxt defs thm =
    1.16    unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
    1.17  
    1.18 -fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss =
    1.19 -  prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss;
    1.20 +fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
    1.21 +  prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
    1.22  
    1.23  fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
    1.24 -    disc_excludes =
    1.25 +    distinct_discs =
    1.26    HEADGOAL (rtac iffI THEN'
    1.27      rtac fun_exhaust THEN'
    1.28      K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
    1.29 @@ -121,7 +121,7 @@
    1.30              rtac FalseE THEN'
    1.31              (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
    1.32               cut_tac fun_disc') THEN'
    1.33 -            dresolve_tac disc_excludes THEN' etac notE THEN' atac)
    1.34 +            dresolve_tac distinct_discs THEN' etac notE THEN' atac)
    1.35        fun_discss) THEN'
    1.36      (etac FalseE ORELSE'
    1.37       resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));