src/Tools/Code/code_thingol.ML
changeset 48442 1d9faa9f65f9
parent 48420 978bd14ad065
child 48445 6b362107e6d9
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Apr 19 07:25:44 2012 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Apr 18 21:47:26 2012 +0200
     1.3 @@ -901,11 +901,11 @@
     1.4    val empty = (empty_naming, Graph.empty);
     1.5  );
     1.6  
     1.7 -fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
     1.8 +fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
     1.9    Program.change_yield (if ignore_cache then NONE else SOME thy)
    1.10      (fn naming_program => (NONE, naming_program)
    1.11 -      |> f thy algebra eqngr name
    1.12 -      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
    1.13 +      |> generate thy algebra eqngr thing
    1.14 +      |-> (fn thing => fn (_, naming_program) => (thing, naming_program)));
    1.15  
    1.16  
    1.17  (* program generation *)