diff -r 74edab16166f -r dd168daf172d src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Thu Feb 02 18:03:35 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Thu Feb 02 18:04:10 2006 +0100
@@ -33,6 +33,7 @@
   val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
   val unfold_const_app: iexpr ->
     (((string * itype) * classlookup list list) * iexpr list) option;
+  val ensure_pat: iexpr -> iexpr;
   val itype_of_iexpr: iexpr -> itype;
 
   val `%% : string * itype list -> itype;
@@ -379,6 +380,13 @@
   | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
   | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
 
+fun ensure_pat (e as IConst (_, [])) = e
+  | ensure_pat (e as IVarE _) = e
+  | ensure_pat (e as IApp (e1, e2)) =
+      (ensure_pat e1 `$ ensure_pat e2; e)
+  | ensure_pat e =
+      error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
+
 fun type_vnames ty = 
   let
     fun extr (IVarT (v, _)) =
@@ -1163,8 +1171,8 @@
 
 fun serialize seri_defs seri_module validate nsp_conn name_root module =
   let
-(*     val resolver = mk_deresolver module nsp_conn snd validate;  *)
-    val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);
+    val resolver = mk_deresolver module nsp_conn snd validate;
+(*     val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);  *)
     fun mk_name prfx name =
       let
         val name_qual = NameSpace.pack (prfx @ [name])
@@ -1177,7 +1185,7 @@
             (mk_name prfx name, mk_contents (prfx @ [name]) modl)
       | seri prfx ds =
           seri_defs (resolver prfx)
-            (map (fn (name, Def def) => (snd (mk_name prfx name), def)) ds)
+            (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
   in
     seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))
       (("", name_root), (mk_contents [] module))