# HG changeset patch
# User krauss
# Date 1256862726 -3600
# Node ID 6343765491647099f2d20526fd3f3ea20dfcb383
# Parent  bb65583ab70d34aa09f66b034472f3722e21abf4
tuned

diff -r bb65583ab70d -r 634376549164 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -486,75 +486,64 @@
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
       end
   in
-      ((map2 requantify intrs intrs_gen, Rdef, forall_intr_vars elim_gen, induct), lthy)
+      ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
-
 fun define_graph Gname fvar domT ranT clauses RCss lthy =
-    let
-      val GT = domT --> ranT --> boolT
-      val (Gvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Gname, GT)])
+  let
+    val GT = domT --> ranT --> boolT
+    val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
 
-      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
-          let
-            fun mk_h_assm (rcfix, rcassm, rcarg) =
-                HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
-                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-                          |> fold_rev (Logic.all o Free) rcfix
-          in
-            HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
-                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
-                      |> fold_rev (curry Logic.mk_implies) gs
-                      |> fold_rev Logic.all (fvar :: qs)
-          end
+    fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
+      let
+        fun mk_h_assm (rcfix, rcassm, rcarg) =
+          HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
+          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+          |> fold_rev (Logic.all o Free) rcfix
+      in
+        HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
+        |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
+        |> fold_rev (curry Logic.mk_implies) gs
+        |> fold_rev Logic.all (fvar :: qs)
+      end
 
-      val G_intros = map2 mk_GIntro clauses RCss
-
-      val ((GIntro_thms, G, G_elim, G_induct), lthy) =
-        inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
-    in
-      ((G, GIntro_thms, G_elim, G_induct), lthy)
-    end
-
-
+    val G_intros = map2 mk_GIntro clauses RCss
+  in
+    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
+  end
 
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
-    let
-      val f_def =
-          Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
-                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
-              |> Syntax.check_term lthy
-
-      val ((f, (_, f_defthm)), lthy) =
-        LocalTheory.define Thm.internalK
-          ((Binding.name (function_name fname), mixfix),
-            ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
-    in
-      ((f, f_defthm), lthy)
-    end
-
+  let
+    val f_def =
+      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 
+        $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
+      |> Syntax.check_term lthy
+  in
+    LocalTheory.define Thm.internalK
+      ((Binding.name (function_name fname), mixfix),
+        ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
+  end
 
 fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
-    let
-
-      val RT = domT --> domT --> boolT
-      val (Rvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Rname, RT)])
+  let
+    val RT = domT --> domT --> boolT
+    val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
 
-      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-          HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
-                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-                    |> fold_rev (curry Logic.mk_implies) gs
-                    |> fold_rev (Logic.all o Free) rcfix
-                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
+    fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
+      HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
+      |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+      |> fold_rev (curry Logic.mk_implies) gs
+      |> fold_rev (Logic.all o Free) rcfix
+      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+      (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
 
-      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
+    val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-      val ((RIntro_thms, R, R_elim, _), lthy) =
-        inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
-    in
-      ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
-    end
+    val ((R, RIntro_thms, R_elim, _), lthy) =
+      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+  in
+    ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
+  end
 
 
 fun fix_globals domT ranT fvar ctxt =
@@ -930,7 +919,7 @@
       val ((G, GIntro_thms, G_elim, G_induct), lthy) =
           PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
-      val ((f, f_defthm), lthy) =
+      val ((f, (_, f_defthm)), lthy) =
           PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
       val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss