diff -r df3c9aa6c9dc -r 1d9faa9f65f9 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Apr 19 07:25:44 2012 +0100 +++ b/src/Tools/Code/code_thingol.ML Wed Apr 18 21:47:26 2012 +0200 @@ -901,11 +901,11 @@ val empty = (empty_naming, Graph.empty); ); -fun invoke_generation ignore_cache thy (algebra, eqngr) f name = +fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing = Program.change_yield (if ignore_cache then NONE else SOME thy) (fn naming_program => (NONE, naming_program) - |> f thy algebra eqngr name - |-> (fn name => fn (_, naming_program) => (name, naming_program))); + |> generate thy algebra eqngr thing + |-> (fn thing => fn (_, naming_program) => (thing, naming_program))); (* program generation *)