diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_simp.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -52,7 +52,7 @@
 
 (* build simpset and conversion from program *)
 
-fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
+fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
       ss
       |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
       |> fold Simplifier.add_cong (the_list some_cong)
@@ -61,7 +61,7 @@
       |> fold Simplifier.add_simp (map (fst o snd) inst_params)
   | add_stmt _ ss = ss;
 
-val add_program = Graph.fold (add_stmt o fst o snd);
+val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
 
 fun simp_ctxt_program thy some_ss program =
   simp_ctxt_default thy some_ss
@@ -77,7 +77,7 @@
 (* evaluation with dynamic code context *)
 
 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
-  (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
+  (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
 
 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);