# HG changeset patch
# User haftmann
# Date 1257952768 -3600
# Node ID ecc90891c47415ada12811baf2f9a80065e0d974
# Parent  43bf5773f92aca1aa9541196ba30556c949dddd7# Parent  ad27f52ee759c2770678be413bfc57f910d2aa0a
merged

diff -r 43bf5773f92a -r ecc90891c474 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Nov 11 15:43:03 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Nov 11 16:19:28 2009 +0100
@@ -30,8 +30,8 @@
     | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
       (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
     | _ => raise Match
-                 
-                 
+
+
 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
     let
       val (n, body) = Term.dest_abs a
@@ -39,7 +39,7 @@
       (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",_) $ _)) = 
@@ -50,7 +50,7 @@
       (v :: vs, b')
     end
   | dest_all_all t = ([],t)
-                     
+
 
 (* FIXME: similar to Variable.focus *)
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
@@ -161,9 +161,9 @@
    Goal.prove_internal []
      (cterm_of thy
        (Logic.mk_equals (t,
-          if is = []
+          if null is
           then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
-          else if js = []
+          else if null js
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
      (K (rewrite_goals_tac ac
diff -r 43bf5773f92a -r ecc90891c474 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 11 15:43:03 2009 +0100
+++ b/src/HOL/Tools/record.ML	Wed Nov 11 16:19:28 2009 +0100
@@ -1754,11 +1754,12 @@
 
     val ([inject', induct', surjective', split_meta'], thm_thy) =
       defs_thy
-      |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
+      |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
            [("ext_inject", inject),
             ("ext_induct", induct),
             ("ext_surjective", surject),
-            ("ext_split", split_meta)];
+            ("ext_split", split_meta)])
+      ||> Code.add_default_eqn ext_def;
 
   in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
 
diff -r 43bf5773f92a -r ecc90891c474 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Wed Nov 11 15:43:03 2009 +0100
+++ b/src/HOL/ex/Records.thy	Wed Nov 11 16:19:28 2009 +0100
@@ -334,4 +334,8 @@
   done
 
 
+subsection {* Some code generation *}
+
+export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+
 end