Fix broken parts of basis

Author: myreen

Diff for: basis/ListProgScript.sml

@@ -63,9 +63,16 @@ val result = translate TL_DEF;
 val result = translate LAST_DEF;
 
 val _ = next_ml_names := ["getItem"];
-val result = translate getItem_def;
+val result = translate mllistTheory.getItem_def;
 
-val result = translate (EL |> REWRITE_RULE[GSYM nth_def]);
+Triviality nth_thm:
+  mllist$nth l 0 = HD l ∧
+  mllist$nth l (SUC n) = mllist$nth (TL l) n
+Proof
+  gvs [mllistTheory.nth_def,listTheory.EL]
+QED
+
+val result = translate nth_thm;
 val nth_side_def = theorem"nth_side_def";
 
 val result = translate (TAKE_def |> REWRITE_RULE[GSYM take_def]);

Diff for: characteristic/cfLetAutoLib.sml

@@ -1692,7 +1692,7 @@ fun xlet_simp_spec asl app_info let_pre app_spec =
       (final_spec, frame_hpl)
   end
   handle HOL_ERR{message = msg, origin_function = fname,
-                 origin_structure  = sname} => raise (ERR "xlet_simp_spec" msg);
+                 origin_structure  = sname, ...} => raise (ERR "xlet_simp_spec" msg);
 
 (* [xlet_mk_post_conditions] *)
 fun xlet_mk_post_condition asl frame_hpl app_spec =
@@ -1921,7 +1921,7 @@ fun xlet_auto_spec (opt_spec : thm option) (g as (asl, w)) =
 (* [xlet_auto] *)
 fun xlet_auto (g as (asl, w)) =
   xlet_auto_spec NONE g
-  handle HOL_ERR {origin_structure = _, origin_function = fname, message = msg}
+  handle HOL_ERR {message = msg, ...}
          => raise (ERR "xlet_auto" msg);
 
 end