# HG changeset patch
# User haftmann
# Date 1262702101 -3600
# Node ID 5b3958210c35d228fe7773db4e509cc8b4ed43ac
# Parent  8e36b3ac6083ad8d891f4cfd3d92a6ac7ded6f44# Parent  95df5e6dd41c82383039a41b63d56f6e339309e9
merged

diff -r 8e36b3ac6083 -r 5b3958210c35 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jan 05 13:34:53 2010 +0100
+++ b/src/Pure/Isar/code.ML	Tue Jan 05 15:35:01 2010 +0100
@@ -317,9 +317,14 @@
   let
     val (tycos, _) = (the_signatures o the_exec) thy;
     val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
-      |> apsnd (Symtab.fold (fn (tyco, n) =>
-          Symtab.update (tyco, Type.LogicalType n)) tycos);
-  in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
+      |> snd 
+      |> Symtab.fold (fn (tyco, n) =>
+          Symtab.update (tyco, Type.LogicalType n)) tycos;
+  in
+    Type.empty_tsig
+    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming
+        (Binding.qualified_name tyco, n) | _ => I) decls
+  end;
 
 fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
diff -r 8e36b3ac6083 -r 5b3958210c35 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jan 05 13:34:53 2010 +0100
+++ b/src/Pure/type.ML	Tue Jan 05 15:35:01 2010 +0100
@@ -19,7 +19,6 @@
     types: decl Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
-  val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
diff -r 8e36b3ac6083 -r 5b3958210c35 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Jan 05 13:34:53 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML	Tue Jan 05 15:35:01 2010 +0100
@@ -116,16 +116,10 @@
           end
       | print_case tyvars thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
-    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
+    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            val n = (length o fst o Code_Thingol.unfold_fun) ty;
-          in
-            Pretty.chunks [
-              semicolon [
-                (str o suffix " ::" o deresolve_base) name,
-                print_typscheme tyvars (vs, ty)
-              ],
+            fun print_err n =
               semicolon (
                 (str o deresolve_base) name
                 :: map str (replicate n "_")
@@ -133,13 +127,7 @@
                 :: str "error"
                 @@ (str o ML_Syntax.print_string
                     o Long_Name.base_name o Long_Name.qualifier) name
-              )
-            ]
-          end
-      | print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
-          let
-            val eqs = filter (snd o snd) raw_eqs;
-            val tyvars = intro_vars (map fst vs) reserved;
+              );
             fun print_eqn ((ts, t), (thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
@@ -162,7 +150,9 @@
                 (str o suffix " ::" o deresolve_base) name,
                 print_typscheme tyvars (vs, ty)
               ]
-              :: map print_eqn eqs
+              :: (case filter (snd o snd) raw_eqs
+               of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
+                | eqs => map print_eqn eqs)
             )
           end
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
diff -r 8e36b3ac6083 -r 5b3958210c35 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Tue Jan 05 13:34:53 2010 +0100
+++ b/src/Tools/Code/lib/Tools/codegen	Tue Jan 05 15:35:01 2010 +0100
@@ -62,4 +62,4 @@
 
 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
-"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
+"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1