# HG changeset patch
# User haftmann
# Date 1135064323 -3600
# Node ID b35d7312c64fb9aed030bda95814bd10f4df9c57
# Parent  7488d8ea61bcdf5f83ef99e5bba048d5b739866e
resolved shadowing of Library.find_first

diff -r 7488d8ea61bc -r b35d7312c64f src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 20 08:38:10 2005 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 20 08:38:43 2005 +0100
@@ -229,11 +229,11 @@
 in
 
 (*Find first term that matches u*)
-fun find_first past u []         = raise TERM("find_first", [])
-  | find_first past u (t::terms) =
+fun find_first_t past u []         = raise TERM ("find_first_t", [])
+  | find_first_t past u (t::terms) =
         if u aconv t then (rev past @ terms)
-        else find_first (t::past) u terms
-        handle TERM _ => find_first (t::past) u terms;
+        else find_first_t (t::past) u terms
+        handle TERM _ => find_first_t (t::past) u terms;
 
 (** Final simplification for the CancelFactor simprocs **)
 val simplify_one = 
@@ -251,7 +251,7 @@
   val dest_sum          = dest_prod
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
-  val find_first        = find_first []
+  val find_first        = find_first_t []
   val trans_tac         = fn _ => trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
diff -r 7488d8ea61bc -r b35d7312c64f src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Tue Dec 20 08:38:10 2005 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue Dec 20 08:38:43 2005 +0100
@@ -354,11 +354,11 @@
   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
 
 (*Find first term that matches u*)
-fun find_first past u []         = raise TERM("find_first", [])
-  | find_first past u (t::terms) =
+fun find_first_t past u []         = raise TERM("find_first_t", [])
+  | find_first_t past u (t::terms) =
         if u aconv t then (rev past @ terms)
-        else find_first (t::past) u terms
-        handle TERM _ => find_first (t::past) u terms;
+        else find_first_t (t::past) u terms
+        handle TERM _ => find_first_t (t::past) u terms;
 
 (** Final simplification for the CancelFactor simprocs **)
 val simplify_one = 
@@ -374,7 +374,7 @@
   val dest_sum          = dest_prod
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
-  val find_first        = find_first []
+  val find_first        = find_first_t []
   val trans_tac         = fn _ => trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))