# HG changeset patch
# User wenzelm
# Date 1165775848 -3600
# Node ID 093ca3efb13249cdb9dd98033b82280deed8f2a3
# Parent  09f62e99859ec234e904c4032e1aca9cf9e24d79
HOLogic cleanup;

diff -r 09f62e99859e -r 093ca3efb132 src/HOL/Tools/function_package/lexicographic_order.ML
--- 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))
diff -r 09f62e99859e -r 093ca3efb132 src/HOL/ex/CodeEmbed.thy
--- 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)) =
diff -r 09f62e99859e -r 093ca3efb132 src/HOL/ex/reflection.ML
--- 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'