merged

--- a/src/Tools/Code/code_simp.ML	Fri Jul 16 13:58:29 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Jul 16 13:58:37 2010 +0200
@@ -57,7 +57,7 @@
       ss addsimps (map (fst o snd) classparam_instances)
   | add_stmt _ ss = ss;
 
-val add_program = Graph.fold (add_stmt o fst o snd)
+val add_program = Graph.fold (add_stmt o fst o snd);
 
 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
   (add_program program (simpset_default thy some_ss));

--- a/src/Tools/Code/code_target.ML	Fri Jul 16 13:58:29 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Jul 16 13:58:37 2010 +0200
@@ -425,32 +425,32 @@
 fun read_inst thy (raw_tyco, raw_class) =
   (read_class thy raw_class, read_tyco thy raw_tyco);
 
-fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
+fun gen_add_syntax (mapp, upd, del) prep_x prep_syn check target raw_x some_raw_syn thy =
   let
-    val x = prep_x thy raw_x |> tap (check_x thy);
-    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
+    val x = prep_x thy raw_x;
+    fun make_syn raw_syn = (check thy x raw_syn: unit; prep_syn raw_syn);
   in case some_raw_syn
-   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
+   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, make_syn raw_syn)) thy
     | NONE => (map_name_syntax target o mapp) (del x) thy
   end;
 
 fun gen_add_syntax_class prep_class =
-  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
+  gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class I ((K o K o K) ());
 
 fun gen_add_syntax_inst prep_inst =
-  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
+  gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst I ((K o K o K) ());
 
 fun gen_add_syntax_tyco prep_tyco =
-  gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
+  gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco I
     (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
-      else ()) ((K o K o K) ()) I prep_tyco;
+      else ());
 
-fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
-  gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
+fun gen_add_syntax_const prep_const prep_syn check_raw_syn =
+  gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const prep_syn
     (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
       then error ("Too many arguments in syntax for constant " ^ quote c)
-      else ()) check_raw_syn prep_syn prep_const;
+      else ()) check_raw_syn;
 
 fun add_reserved target =
   let
@@ -510,8 +510,8 @@
 val add_syntax_class = gen_add_syntax_class cert_class;
 val add_syntax_inst = gen_add_syntax_inst cert_inst;
 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
-val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
+val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
+val add_syntax_const = gen_add_syntax_const (K I) I;
 val allow_abort = gen_allow_abort (K I);
 val add_reserved = add_reserved;
 val add_include = add_include;
@@ -519,8 +519,8 @@
 val add_syntax_class_cmd = gen_add_syntax_class read_class;
 val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
+val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
 
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 

--- a/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:58:29 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:58:37 2010 +0200
@@ -222,10 +222,12 @@
         val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
-fun eta_expand k (c as (_, (_, tys)), ts) =
+fun eta_expand k (c as (name, (_, tys)), ts) =
   let
     val j = length ts;
     val l = k - j;
+    val _ = if l > length tys
+      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
       (Name.names ctxt "a" ((take l o drop j) tys));