src/HOL/Boogie/Tools/boogie_vcs.ML
changeset 39020 ac0f24f850c9
parent 38795 848be46708dc
child 39687 4e9b6ada3a21
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -348,6 +348,6 @@
   let
     fun rewr (_, (t, _)) = vc_of_term (f thy t)
       |> (fn vc => (vc, (t, thm_of thy vc)))
-  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
+  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map (K rewr) vcs, g))) thy end
 
 end