src/Tools/Code/code_target.ML
changeset 47576 b32aae03e3d6
parent 47089 29e92b644d6c
child 48371 3a5a5a992519
--- a/src/Tools/Code/code_target.ML	Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Apr 19 10:16:51 2012 +0200
@@ -270,7 +270,7 @@
 
 fun activate_target thy target =
   let
-    val ((targets, abortable), default_width) = Targets.get thy;
+    val ((_, abortable), default_width) = Targets.get thy;
     val (modify, data) = collapse_hierarchy thy target;
   in (default_width, abortable, data, modify) end;
 
@@ -630,7 +630,7 @@
 
 local
 
-fun zip_list (x::xs) f g =
+fun zip_list (x :: xs) f g =
   f
   :|-- (fn y =>
     fold_map (fn x => g |-- f >> pair x) xs