# HG changeset patch
# User krauss
# Date 1287783920 -7200
# Node ID 6f012a209dac44c2e61d655c9ee2f735be966545
# Parent  1c75f3f192ae30b09bb9c1758484da4eb58cc11e
some cleanup in Function_Lib

diff -r 1c75f3f192ae -r 6f012a209dac src/HOL/Tools/Function/function.ML
--- 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',
diff -r 1c75f3f192ae -r 6f012a209dac src/HOL/Tools/Function/function_lib.ML
--- 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;
diff -r 1c75f3f192ae -r 6f012a209dac src/HOL/Tools/Function/mutual.ML
--- 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,