1.1 --- a/src/Pure/Isar/code.ML	Tue Jan 05 13:34:53 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jan 05 15:35:01 2010 +0100
     1.3 @@ -317,9 +317,14 @@
     1.4    let
     1.5      val (tycos, _) = (the_signatures o the_exec) thy;
     1.6      val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
     1.7 -      |> apsnd (Symtab.fold (fn (tyco, n) =>
     1.8 -          Symtab.update (tyco, Type.LogicalType n)) tycos);
     1.9 -  in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
    1.10 +      |> snd 
    1.11 +      |> Symtab.fold (fn (tyco, n) =>
    1.12 +          Symtab.update (tyco, Type.LogicalType n)) tycos;
    1.13 +  in
    1.14 +    Type.empty_tsig
    1.15 +    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming
    1.16 +        (Binding.qualified_name tyco, n) | _ => I) decls
    1.17 +  end;
    1.18  
    1.19  fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
    1.20  

     2.1 --- a/src/Pure/type.ML	Tue Jan 05 13:34:53 2010 +0100
     2.2 +++ b/src/Pure/type.ML	Tue Jan 05 15:35:01 2010 +0100
     2.3 @@ -19,7 +19,6 @@
     2.4      types: decl Name_Space.table,
     2.5      log_types: string list}
     2.6    val empty_tsig: tsig
     2.7 -  val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig
     2.8    val defaultS: tsig -> sort
     2.9    val logical_types: tsig -> string list
    2.10    val eq_sort: tsig -> sort * sort -> bool

     3.1 --- a/src/Tools/Code/code_haskell.ML	Tue Jan 05 13:34:53 2010 +0100
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jan 05 15:35:01 2010 +0100
     3.3 @@ -116,16 +116,10 @@
     3.4            end
     3.5        | print_case tyvars thm vars fxy ((_, []), _) =
     3.6            (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
     3.7 -    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
     3.8 +    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
     3.9            let
    3.10              val tyvars = intro_vars (map fst vs) reserved;
    3.11 -            val n = (length o fst o Code_Thingol.unfold_fun) ty;
    3.12 -          in
    3.13 -            Pretty.chunks [
    3.14 -              semicolon [
    3.15 -                (str o suffix " ::" o deresolve_base) name,
    3.16 -                print_typscheme tyvars (vs, ty)
    3.17 -              ],
    3.18 +            fun print_err n =
    3.19                semicolon (
    3.20                  (str o deresolve_base) name
    3.21                  :: map str (replicate n "_")
    3.22 @@ -133,13 +127,7 @@
    3.23                  :: str "error"
    3.24                  @@ (str o ML_Syntax.print_string
    3.25                      o Long_Name.base_name o Long_Name.qualifier) name
    3.26 -              )
    3.27 -            ]
    3.28 -          end
    3.29 -      | print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
    3.30 -          let
    3.31 -            val eqs = filter (snd o snd) raw_eqs;
    3.32 -            val tyvars = intro_vars (map fst vs) reserved;
    3.33 +              );
    3.34              fun print_eqn ((ts, t), (thm, _)) =
    3.35                let
    3.36                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    3.37 @@ -162,7 +150,9 @@
    3.38                  (str o suffix " ::" o deresolve_base) name,
    3.39                  print_typscheme tyvars (vs, ty)
    3.40                ]
    3.41 -              :: map print_eqn eqs
    3.42 +              :: (case filter (snd o snd) raw_eqs
    3.43 +               of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
    3.44 +                | eqs => map print_eqn eqs)
    3.45              )
    3.46            end
    3.47        | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =

     4.1 --- a/src/Tools/Code/lib/Tools/codegen	Tue Jan 05 13:34:53 2010 +0100
     4.2 +++ b/src/Tools/Code/lib/Tools/codegen	Tue Jan 05 15:35:01 2010 +0100
     4.3 @@ -62,4 +62,4 @@
     4.4  
     4.5  FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
     4.6  
     4.7 -"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
     4.8 +"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1