--- a/src/HOL/Tools/function_package/lexicographic_order.ML Sun Dec 10 19:37:27 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Sun Dec 10 19:37:28 2006 +0100
@@ -230,7 +230,7 @@
| SOME order => let
val clean_table = map (fn x => map (nth x) order) table
val funs = map (nth base_funs) order
- val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
+ val list = HOLogic.mk_list (fastype_of var --> HOLogic.natT) funs
val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
val crelterm = cterm_of thy relterm
val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
--- a/src/HOL/ex/CodeEmbed.thy Sun Dec 10 19:37:27 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy Sun Dec 10 19:37:28 2006 +0100
@@ -57,10 +57,10 @@
val typ_sort = Type (Sign.intern_type thy "sort", []);
val typ_typ = Type (Sign.intern_type thy "typ", []);
val typ_term = Type (Sign.intern_type thy "term", []);
- val term_sort = HOLogic.mk_list MLString.term_ml_string typ_class;
+ val term_sort = HOLogic.mk_list typ_class o map MLString.term_ml_string;
fun term_typ f (Type (tyco, tys)) =
Const (const_Type, MLString.typ_ml_string --> HOLogic.listT typ_typ --> typ_typ)
- $ MLString.term_ml_string tyco $ HOLogic.mk_list (term_typ f) typ_typ tys
+ $ MLString.term_ml_string tyco $ HOLogic.mk_list typ_typ (map (term_typ f) tys)
| term_typ f (TFree v) =
f v;
fun term_term f g (Const (c, ty)) =
--- a/src/HOL/ex/reflection.ML Sun Dec 10 19:37:27 2006 +0100
+++ b/src/HOL/ex/reflection.ML Sun Dec 10 19:37:28 2006 +0100
@@ -269,7 +269,7 @@
|> split_last |> fst
val cert = cterm_of (ProofContext.theory_of ctxt)
val cvs = map (fn t => t |> (AList.lookup (op =) (!bds)) |> the |> snd
- |> HOLogic.mk_list I (dest_listT t) |> cert |> SOME)
+ |> HOLogic.mk_list (dest_listT t) |> cert |> SOME)
tys
val th' = (instantiate' [] cvs (th RS sym)) RS sym
val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'