resolved shadowing of Library.find_first
authorhaftmann
Tue Dec 20 08:38:43 2005 +0100 (2005-12-20)
changeset 18442b35d7312c64f
parent 18441 7488d8ea61bc
child 18443 a1d53af4c4c7
resolved shadowing of Library.find_first
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 20 08:38:10 2005 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 20 08:38:43 2005 +0100
     1.3 @@ -229,11 +229,11 @@
     1.4  in
     1.5  
     1.6  (*Find first term that matches u*)
     1.7 -fun find_first past u []         = raise TERM("find_first", [])
     1.8 -  | find_first past u (t::terms) =
     1.9 +fun find_first_t past u []         = raise TERM ("find_first_t", [])
    1.10 +  | find_first_t past u (t::terms) =
    1.11          if u aconv t then (rev past @ terms)
    1.12 -        else find_first (t::past) u terms
    1.13 -        handle TERM _ => find_first (t::past) u terms;
    1.14 +        else find_first_t (t::past) u terms
    1.15 +        handle TERM _ => find_first_t (t::past) u terms;
    1.16  
    1.17  (** Final simplification for the CancelFactor simprocs **)
    1.18  val simplify_one = 
    1.19 @@ -251,7 +251,7 @@
    1.20    val dest_sum          = dest_prod
    1.21    val mk_coeff          = mk_coeff
    1.22    val dest_coeff        = dest_coeff
    1.23 -  val find_first        = find_first []
    1.24 +  val find_first        = find_first_t []
    1.25    val trans_tac         = fn _ => trans_tac
    1.26    val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
    1.27    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
     2.1 --- a/src/HOL/Integ/nat_simprocs.ML	Tue Dec 20 08:38:10 2005 +0100
     2.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Dec 20 08:38:43 2005 +0100
     2.3 @@ -354,11 +354,11 @@
     2.4    | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
     2.5  
     2.6  (*Find first term that matches u*)
     2.7 -fun find_first past u []         = raise TERM("find_first", [])
     2.8 -  | find_first past u (t::terms) =
     2.9 +fun find_first_t past u []         = raise TERM("find_first_t", [])
    2.10 +  | find_first_t past u (t::terms) =
    2.11          if u aconv t then (rev past @ terms)
    2.12 -        else find_first (t::past) u terms
    2.13 -        handle TERM _ => find_first (t::past) u terms;
    2.14 +        else find_first_t (t::past) u terms
    2.15 +        handle TERM _ => find_first_t (t::past) u terms;
    2.16  
    2.17  (** Final simplification for the CancelFactor simprocs **)
    2.18  val simplify_one = 
    2.19 @@ -374,7 +374,7 @@
    2.20    val dest_sum          = dest_prod
    2.21    val mk_coeff          = mk_coeff
    2.22    val dest_coeff        = dest_coeff
    2.23 -  val find_first        = find_first []
    2.24 +  val find_first        = find_first_t []
    2.25    val trans_tac         = fn _ => trans_tac
    2.26    val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
    2.27    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))