src/Tools/Code/code_simp.ML

   end;
 
 
 (* 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)
   | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
       ss
       |> 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
   |> add_program program;
 

 
 
 (* 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);
 
 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;