--- a/src/HOL/Tools/Function/function.ML Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Fri Oct 22 23:45:20 2010 +0200
@@ -108,8 +108,9 @@
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
- ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
- ||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
+ ||> (case trsimps of NONE => I | SOME thms =>
+ addsmps I "simps" I simp_attribs thms #> snd
+ #> Spec_Rules.add Spec_Rules.Equational (fs, thms))
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
@@ -117,7 +118,8 @@
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
||> (snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
- ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
+ ||> (case domintros of NONE => I | SOME thms =>
+ Local_Theory.note ((qualify "domintros", []), thms) #> snd)
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
--- a/src/HOL/Tools/Function/function_lib.ML Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Oct 22 23:45:20 2010 +0200
@@ -8,29 +8,15 @@
structure Function_Lib = (* FIXME proper signature *)
struct
-fun map_option f NONE = NONE
- | map_option f (SOME x) = SOME (f x);
-
-fun fold_option f NONE y = y
- | fold_option f (SOME x) y = f x y;
-
-(* Ex: "The variable" ^ plural " is" "s are" vs *)
+(* "The variable" ^ plural " is" "s are" vs *)
fun plural sg pl [x] = sg
| plural sg pl _ = pl
-fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
- let
- val (n, body) = Term.dest_abs a
- in
- (Free (n, T), body)
- end
- | dest_all _ = raise Match
-
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
fun dest_all_all (t as (Const ("all",_) $ _)) =
let
- val (v,b) = dest_all t
+ val (v,b) = Logic.dest_all t |> apfst Free
val (vs, b') = dest_all_all b
in
(v :: vs, b')
@@ -56,18 +42,10 @@
(ctx, [], t)
-fun map3 _ [] [] [] = []
- | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
- | map3 _ _ _ _ = raise Library.UnequalLengths;
-
fun map4 _ [] [] [] [] = []
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
| map4 _ _ _ _ _ = raise Library.UnequalLengths;
-fun map6 _ [] [] [] [] [] [] = []
- | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
- | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
-
fun map7 _ [] [] [] [] [] [] [] = []
| map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
| map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
--- a/src/HOL/Tools/Function/mutual.ML Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Fri Oct 22 23:45:20 2010 +0200
@@ -267,10 +267,10 @@
val rew_ss = HOL_basic_ss addsimps all_f_defs
val mpsimps = map2 mk_mpsimp fqgars psimps
- val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
+ val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
val mtermination = full_simplify rew_ss termination
- val mdomintros = map_option (map (full_simplify rew_ss)) domintros
+ val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
in
FunctionResult { fs=fs, G=G, R=R,
psimps=mpsimps, simple_pinducts=minducts,