# HG changeset patch # User wenzelm # Date 1181076416 -7200 # Node ID 851b8ea067ac012cf429758c5c2f3724999432df # Parent 572a483de1b058f4ed75f4947b8814fa0822c159 simplified/renamed add_numerals; diff -r 572a483de1b0 -r 851b8ea067ac src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Tue Jun 05 22:46:55 2007 +0200 +++ b/src/HOL/Library/EfficientNat.thy Tue Jun 05 22:46:56 2007 +0200 @@ -225,7 +225,7 @@ |> SOME else NONE in - fold (HOLogic.add_numerals_of o Thm.term_of) cts [] + fold (HOLogic.add_numerals o Thm.term_of) cts [] |> map_filter mk_rew end; *} diff -r 572a483de1b0 -r 851b8ea067ac src/HOL/hologic.ML --- a/src/HOL/hologic.ML Tue Jun 05 22:46:55 2007 +0200 +++ b/src/HOL/hologic.ML Tue Jun 05 22:46:56 2007 +0200 @@ -87,7 +87,7 @@ val mk_numeral: integer -> term val dest_numeral: term -> integer val number_of_const: typ -> term - val add_numerals_of: term -> (term * typ) list -> (term * typ) list + val add_numerals: term -> (term * typ) list -> (term * typ) list val mk_number: typ -> integer -> term val dest_number: term -> typ * integer val realT: typ @@ -351,21 +351,10 @@ fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T); -fun add_numerals_of (Const _) = - I - | add_numerals_of (Var _) = - I - | add_numerals_of (Free _) = - I - | add_numerals_of (Bound _) = - I - | add_numerals_of (Abs (_, _, t)) = - add_numerals_of t - | add_numerals_of (t as _ $ _) = - case strip_comb t - of (Const ("Numeral.number_class.number_of", - Type (_, [_, T])), ts) => fold (cons o rpair T) ts - | (t', ts) => add_numerals_of t' #> fold add_numerals_of ts; +fun add_numerals (Const ("Numeral.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T) + | add_numerals (t $ u) = add_numerals t #> add_numerals u + | add_numerals (Abs (_, _, t)) = add_numerals t + | add_numerals _ = I; fun mk_number T 0 = Const ("HOL.zero_class.zero", T) | mk_number T 1 = Const ("HOL.one_class.one", T)