equal
deleted
inserted
replaced
899 ( |
899 ( |
900 type T = naming * program; |
900 type T = naming * program; |
901 val empty = (empty_naming, Graph.empty); |
901 val empty = (empty_naming, Graph.empty); |
902 ); |
902 ); |
903 |
903 |
904 fun invoke_generation ignore_cache thy (algebra, eqngr) f name = |
904 fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing = |
905 Program.change_yield (if ignore_cache then NONE else SOME thy) |
905 Program.change_yield (if ignore_cache then NONE else SOME thy) |
906 (fn naming_program => (NONE, naming_program) |
906 (fn naming_program => (NONE, naming_program) |
907 |> f thy algebra eqngr name |
907 |> generate thy algebra eqngr thing |
908 |-> (fn name => fn (_, naming_program) => (name, naming_program))); |
908 |-> (fn thing => fn (_, naming_program) => (thing, naming_program))); |
909 |
909 |
910 |
910 |
911 (* program generation *) |
911 (* program generation *) |
912 |
912 |
913 fun consts_program thy permissive consts = |
913 fun consts_program thy permissive consts = |