author haftmann Wed, 11 Nov 2009 16:19:28 +0100 changeset 33614 ecc90891c474 parent 33610 43bf5773f92a (current diff) parent 33613 ad27f52ee759 (diff) child 33616 69f0a6271825
merged
--- 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
--- 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)])

in (thm_thy, extT, induct', inject', split_meta', ext_def) end;

--- 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